⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hn'0 < ↑n : (0ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) < (nℕ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) := Nat.cast_posNat.cast_pos.{u_3} {α : Type u_3} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ} :
  0 < ↑n ↔ 0 < nSpecialisation of `Nat.cast_pos'`, which seems to be easier for Lean to use. .2Iff.mpr {a b : Prop} (self : a ↔ b) : b → aModus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`.  hn1 ≤ n
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 h‖↑(↑n + 1) ^ (-s) - ↑↑n ^ (-s)‖ ≤ ‖-s‖ * (↑n + 1 - ↑n) * ↑n ^ ((-s).re - 1) := norm_ofReal_cpow_sub_ofReal_cpow_leComplex.norm_ofReal_cpow_sub_ofReal_cpow_le {r : ℂ} (hr : r.re ≤ 1) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
  ‖↑b ^ r - ↑a ^ r‖ ≤ ‖r‖ * (b - a) * a ^ (r.re - 1)**FTC increment bound** for complex powers of positive reals: if `r.re ≤ 1` and
`0 < a ≤ b`, then `‖(b : ℂ) ^ r - (a : ℂ) ^ r‖ ≤ ‖r‖ * (b - a) * a ^ (r.re - 1)`.
The difference is the integral of the derivative `r * x ^ (r - 1)`, whose norm on `[a, b]`
is at most `‖r‖ * a ^ (r.re - 1)` because `x ↦ x ^ (r.re - 1)` is antitone for
`r.re - 1 ≤ 0`.  (r := -sℂ)
    (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [neg_reComplex.neg_re (z : ℂ) : (-z).re = -z.re]; linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
) hn'0 < ↑n (le_add_of_nonneg_rightle_add_of_nonneg_right.{u_1} {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftMono α] {a b : α} (h : 0 ≤ b) : a ≤ a + b zero_le_onezero_le_one.{u_1} {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] : 0 ≤ 1`zero_le_one` with the type argument implicit. )
  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [norm_sub_revnorm_sub_rev.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖ = ‖b - a‖] atLocation specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
 h‖↑(↑n + 1) ^ (-s) - ↑↑n ^ (-s)‖ ≤ ‖-s‖ * (↑n + 1 - ↑n) * ↑n ^ ((-s).re - 1)
  simpaThis is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 [add_sub_cancel_leftadd_sub_cancel_left.{u_3} {G : Type u_3} [AddCommGroup G] (a b : G) : a + b - a = b] usingThe arguments to the `simpa` family tactics.  h‖↑↑n ^ (-s) - ↑(↑n + 1) ^ (-s)‖ ≤ ‖-s‖ * (↑n + 1 - ↑n) * ↑n ^ ((-s).re - 1)

≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
 Summable.of_norm_bounded_eventually_nat
    (g := fun n : ℕ ↦ C * R * (n : ℝ) ^ (-δ - 1))
    ((Real.summable_nat_rpow.2 (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
)).mul_left _) ?_
  filter_upwards`filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms
`h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`.
The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for
`{ filter_upwards [h₁, ⋯, hₙ], intro a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for
`{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`.
Note that in this case, the `aᵢ` terms can be used in `e`.
 [eventually_ge_atTop 1] with`filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms
`h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`.
The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for
`{ filter_upwards [h₁, ⋯, hₙ], intro a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for
`{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`.
Note that in this case, the `aᵢ` terms can be used in `e`.
 n hn
  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [if_neg (Nat.one_le_iff_ne_zero.mp hn), Real.norm_eq_abs, abs_of_nonneg
    (mul_nonneg (mul_nonneg hC0 hR0) (Real.rpow_nonneg (Nat.cast_nonneg n) _))]

≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  rcases`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 Nat.eq_zero_or_pos n with`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 rfl | hn
  · -- `n = 0`: on the box the term is the constant `(f 0) * (0 - 1)`
    refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
 (differentiableOn_const ((∑ k ∈ Finset.range (0 + 1), f k) * (0 - 1))).congr ?_
    introIntroduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.

* `intro` by itself introduces one anonymous hypothesis, which can be accessed
  by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
  can be anonymized via `_`, given a type ascription, or matched against a pattern:
  ```lean
  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  ```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
  is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
  ```lean
  intro
  | n + 1, 0 => tac
  | ...
  ```
 w hw
    haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hw0 : -w ≠ 0 := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
      rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [ne_eq, neg_eq_zero]
      rintroThe `rintro` tactic is a combination of the `intros` tactic with `rcases` to
allow for destructuring patterns while introducing variables. See `rcases` for
a description of supported patterns. For example, `rintro (a | ⟨b, c⟩) ⟨d, e⟩`
will introduce two variables, and then do case splits on both of them producing
two subgoals, one with variables `a d e` and the other with `b c d e`.

`rintro`, unlike `rcases`, also supports the form `(x y : ty)` for introducing
and type-ascripting multiple variables at once, similar to binders.
 rfl
      haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 : δ < (0 : ℂ).re := hw.1
      rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [Complex.zero_re] atLocation specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
 this
      linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.

    simpThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 [Complex.zero_cpow hw0]
  · haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hne : ((n : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.2 hn.ne'
    haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hne1 : ((n : ℕ) : ℂ) + 1 ≠ 0 := Nat.cast_add_one_ne_zero n
    exact`exact e` closes the main goal if its target type matches that of `e`.
 (((differentiable_neg.const_cpow (Or.inl hne)).sub
      (differentiable_neg.const_cpow (Or.inl hne1))).const_mul _).differentiableOn

≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hC0 : 0 ≤ C := (norm_nonneg _).trans (hC 0)
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hwre : δ < w.re := hw.1
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hwnorm : ‖w‖ < R := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
    haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 := hw.2
    rwa`rwa` is short-hand for `rw; assumption`.  [Metric.mem_ball, dist_zero_right] atLocation specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
 this
  rcases`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 Nat.eq_zero_or_pos n with`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 rfl | hn
  · rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [if_pos rfl]
    haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hw0 : -w ≠ 0 := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
      rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [ne_eq, neg_eq_zero]
      rintroThe `rintro` tactic is a combination of the `intros` tactic with `rcases` to
allow for destructuring patterns while introducing variables. See `rcases` for
a description of supported patterns. For example, `rintro (a | ⟨b, c⟩) ⟨d, e⟩`
will introduce two variables, and then do case splits on both of them producing
two subgoals, one with variables `a d e` and the other with `b c d e`.

`rintro`, unlike `rcases`, also supports the form `(x y : ty)` for introducing
and type-ascripting multiple variables at once, similar to binders.
 rfl
      rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [Complex.zero_re] atLocation specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
 hwre
      linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.

    simpaThis is a "finishing" tactic modification of `simp`. It has two forms.

* `simpa [rules, ⋯] using e` will simplify the goal and the type of
  `e` using `rules`, then try to close the goal using `e`.

  Simplifying the type of `e` makes it more likely to match the goal
  (which has also been simplified). This construction also tends to be
  more robust under changes to the simp lemma set.

  The final match between the simplified `e` and the simplified goal uses
  **reducible** transparency, so it does not unfold semireducible definitions.
  Write `simpa [rules, ⋯] using! e` to perform the match at the ambient
  (default/semireducible) transparency instead.

* `simpa [rules, ⋯]` will simplify the goal and the type of a
  hypothesis `this` if present in the context, then try to close the goal using
  the `assumption` tactic.

As with `simp`, the `!` modifier after `simpa` enables auto-unfolding of
definitions in the simp set.
 [Complex.zero_cpow hw0] usingThe arguments to the `simpa` family tactics.  hC 0
  · rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [if_neg hn.ne']
    haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 h1n : (1 : ℝ) ≤ (n : ℝ) := Nat.one_le_cast.2 hn
    rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [norm_mul]
    calcStep-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 ‖∑ k ∈ Finset.range (n + 1), f k‖ * ‖(n : ℂ) ^ (-w) - ((n : ℂ) + 1) ^ (-w)‖
        ≤ C * (‖w‖ * (n : ℝ) ^ (-w.re - 1)) :=
          mul_le_mul (hC n)
            (Complex.norm_natCast_cpow_sub_add_one_cpow_le (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
) hn)
            (norm_nonneg _) hC0
      _ ≤ C * (R * (n : ℝ) ^ (-δ - 1)) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
          refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
 mul_le_mul_of_nonneg_left ?_ hC0
          exact`exact e` closes the main goal if its target type matches that of `e`.
 mul_le_mul hwnorm.le
            (Real.rpow_le_rpow_of_exponent_le h1n (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  linarith`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving `False`.

In theory, `linarith` should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like `Nat` and `Int`,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.

An example:
```lean
example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith
```

`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
Disequality hypotheses require case splitting and are not normally considered
(see the `splitNe` option below).

`linarith [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.

`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
`h1`, `h2`, `h3`, and proofs `t1`, `t2`, `t3`. It will ignore the rest of the local context.

`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
```lean
example (x : ℚ) : id x ≥ x := by
  linarith
```
will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
This can sometimes be expensive.

`linarith (config := { .. })` takes a config object with five
optional arguments:
* `discharger` specifies a tactic to be used for reducing an algebraic equation in the
  proof stage. The default is `ring`. Other options include `simp` for basic
  problems.
* `transparency` controls how hard `linarith` will try to match atoms to each other. By default
  it will only unfold `reducible` definitions.
* If `splitHypotheses` is true, `linarith` will split conjunctions in the context into separate
  hypotheses.
* If `splitNe` is `true`, `linarith` will case split on disequality hypotheses.
  For a given `x ≠ y` hypothesis, `linarith` is run with both `x < y` and `x > y`,
  and so this runs linarith exponentially many times with respect to the number of
  disequality hypotheses. (`false` by default.)
* If `exfalso` is `false`, `linarith` will fail when the goal is neither an inequality nor `False`.
  (`true` by default.)
* If `minimize` is `false`, `linarith?` will report all hypotheses appearing in its initial
  proof without attempting to drop redundancies. (`true` by default.)
* `restrict_type` (not yet implemented in mathlib4)
  will only use hypotheses that are inequalities over `tp`. This is useful
  if you have e.g. both integer- and rational-valued inequalities in the local context, which can
  sometimes confuse the tactic.

A variant, `nlinarith`, does some basic preprocessing to handle some nonlinear goals.

The option `set_option trace.linarith true` will trace certain intermediate stages of the `linarith`
routine.
))
            (Real.rpow_nonneg (Nat.cast_nonneg n) _) hR0
      _ = C * R * (n : ℝ) ^ (-δ - 1) := (mul_assoc _ _ _).symm

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hC00 ≤ C : 0ℝ ≤ Cℝ := (norm_nonnegnorm_nonneg.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖ _).transLE.le.trans.{u_1} {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c**Alias** of `le_trans`. (hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C 0ℕ)
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hR00 ≤ R : 0ℝ ≤ Rℝ := zero_le_onezero_le_one.{u_1} {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] : 0 ≤ 1`zero_le_one` with the type argument implicit. .transLE.le.trans.{u_1} {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c**Alias** of `le_trans`. hR1 ≤ R
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hVopenIsOpen ({s | δ < s.re} ∩ Metric.ball 0 R) : IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  ({sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  | δℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. } ∩ Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0ℂ Rℝ) :=
    (isOpen_ltisOpen_lt.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
  [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsOpen {b | f b < g b} continuous_constcontinuous_const.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} :
  Continuous fun x => y Complex.continuous_reComplex.continuous_re : Continuous Complex.re).interIsOpen.inter.{u} {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t) Metric.isOpen_ballMetric.isOpen_ball.{u} {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsOpen (Metric.ball x ε)
  exact`exact e` closes the main goal if its target type matches that of `e`.
 Complex.differentiableOn_tsum_of_summable_normComplex.differentiableOn_tsum_of_summable_norm.{u_1, u_2} {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {U : Set ℂ} {F : ι → ℂ → E} [CompleteSpace E] {u : ι → ℝ} (hu : Summable u)
  (hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U) (hU : IsOpen U) (hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i) :
  DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) UIf the terms in the sum `∑' (i : ι), F i` are uniformly bounded on `U` by a
summable function, and each term in the sum is differentiable on `U`, then so is the sum. 
    (summable_bpSeries_boxBoundsummable_bpSeries_boxBound {C R δ : ℝ} (hC0 : 0 ≤ C) (hR0 : 0 ≤ R) (hδ : 0 < δ) :
  Summable fun n => if n = 0 then C else C * R * ↑n ^ (-δ - 1)**Summable majorant for the box `M`-test**: on `{s | δ < s.re} ∩ ball 0 R` (with `δ > 0`,
`0 ≤ R`) the by-parts terms are dominated by `n ↦ if n = 0 then C else C · R · n ^ (-δ - 1)`,
which is summable because `-δ - 1 < -1`.  hC00 ≤ C hR00 ≤ R hδ0 < δ)
    (fun nℕ ↦ differentiableOn_bpSeries_termdifferentiableOn_bpSeries_term {f : ℕ → ℂ} {R δ : ℝ} (hδ : 0 < δ) (n : ℕ) :
  DifferentiableOn ℂ (fun s => (∑ k ∈ Finset.range (n + 1), f k) * (↑n ^ (-s) - (↑n + 1) ^ (-s)))
    ({s | δ < s.re} ∩ Metric.ball 0 R)**Per-term holomorphy on the box**: each by-parts term
`(∑ k ≤ n, f k) · ((n : ℂ) ^ (-s) - (n + 1) ^ (-s))` is holomorphic on
`{s | δ < s.re} ∩ ball 0 R` — a constant when `n = 0`, a difference of complex powers
otherwise.  (R := Rℝ) hδ0 < δ nℕ) hVopenIsOpen ({s | δ < s.re} ∩ Metric.ball 0 R)
    (fun nℕ wℂ hww ∈ {s | δ < s.re} ∩ Metric.ball 0 R ↦ norm_bpSeries_term_le_boxBoundnorm_bpSeries_term_le_boxBound {f : ℕ → ℂ} {C : ℝ} (hC : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C) {R δ : ℝ}
  (hR0 : 0 ≤ R) (hδ : 0 < δ) (n : ℕ) (w : ℂ) (hw : w ∈ {s | δ < s.re} ∩ Metric.ball 0 R) :
  ‖(∑ k ∈ Finset.range (n + 1), f k) * (↑n ^ (-w) - (↑n + 1) ^ (-w))‖ ≤ if n = 0 then C else C * R * ↑n ^ (-δ - 1)**Uniform `M`-test bound on the box**: if the partial sums of `f` are bounded by `C`,
then on `{s | δ < s.re} ∩ ball 0 R` each by-parts term satisfies
`‖term n w‖ ≤ if n = 0 then C else C · R · n ^ (-δ - 1)`.  hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C hR00 ≤ R hδ0 < δ nℕ wℂ hww ∈ {s | δ < s.re} ∩ Metric.ball 0 R)

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  introIntroduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.

* `intro` by itself introduces one anonymous hypothesis, which can be accessed
  by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
  can be anonymized via `_`, given a type ascription, or matched against a pattern:
  ```lean
  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  ```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
  is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
  ```lean
  intro
  | n + 1, 0 => tac
  | ...
  ```
 s₀ℂ hs₀s₀ ∈ {s | 0 < s.re}
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hs₀re0 < s₀.re : 0ℝ < s₀ℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number.  := hs₀s₀ ∈ {s | 0 < s.re}
  obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.

```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```

If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.

If `type` is omitted, `:= proof` is required.
 ⟨δℝ, hδ0 < δ, hδs₀δ < s₀.re⟩ : ∃ δℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. , 0ℝ < δℝ ∧ δℝ < s₀ℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number.  :=
    ⟨Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. s₀ℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number.  / 2ℝ,Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.  half_poshalf_pos.{u_2} {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α]
  (h : 0 < a) : 0 < a / 2 hs₀re0 < s₀.re,Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.  half_lt_selfhalf_lt_self.{u_2} {α : Type u_2} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α] :
  0 < a → a / 2 < a**Alias** of the reverse direction of `half_lt_self_iff`. hs₀re0 < s₀.re⟩Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. 
  obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.

```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```

If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.

If `type` is omitted, `:= proof` is required.
 ⟨Rℝ, hR1 ≤ R, hs₀R‖s₀‖ < R⟩ : ∃ Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. , 1ℝ ≤ Rℝ ∧ ‖s₀ℂ‖ < Rℝ :=
    ⟨Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. ‖s₀ℂ‖ + 1ℝ,Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.  le_add_of_nonneg_leftle_add_of_nonneg_left.{u_1} {α : Type u_1} [AddZeroClass α] [LE α] [AddRightMono α] {a b : α} (h : 0 ≤ b) : a ≤ b + a (norm_nonnegnorm_nonneg.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖ _),Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.  lt_add_onelt_add_one.{u_1} {α : Type u_1} [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
  [AddLeftStrictMono α] (a : α) : a < a + 1 _⟩Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists pExistential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hVopenIsOpen ({s | δ < s.re} ∩ Metric.ball 0 R) : IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  ({sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  | δℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. } ∩ Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0ℂ Rℝ) :=
    (isOpen_ltisOpen_lt.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
  [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : IsOpen {b | f b < g b} continuous_constcontinuous_const.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} :
  Continuous fun x => y Complex.continuous_reComplex.continuous_re : Continuous Complex.re).interIsOpen.inter.{u} {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t) Metric.isOpen_ballMetric.isOpen_ball.{u} {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsOpen (Metric.ball x ε)
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hs₀Vs₀ ∈ {s | δ < s.re} ∩ Metric.ball 0 R : s₀ℂ ∈ {sℂ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.  | δℝ < sℂ.reComplex.re (self : ℂ) : ℝThe real part of a complex number. } ∩ Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0ℂ Rℝ :=
    ⟨And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`And.intro : a → b → a ∧ b` is the constructor for the And operation. hδs₀δ < s₀.re,And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`And.intro : a → b → a ∧ b` is the constructor for the And operation.  by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [Metric.mem_ballMetric.mem_ball.{u} {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist y x < ε, dist_zero_rightdist_zero_right.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : dist a 0 = ‖a‖]; exact`exact e` closes the main goal if its target type matches that of `e`.
 hs₀R‖s₀‖ < R⟩And.intro {a b : Prop} (left : a) (right : b) : a ∧ b`And.intro : a → b → a ∧ b` is the constructor for the And operation. 
  exact`exact e` closes the main goal if its target type matches that of `e`.
 (((differentiableOn_bpSeries_boxdifferentiableOn_bpSeries_box {f : ℕ → ℂ} {C : ℝ} (hC : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C) {δ R : ℝ}
  (hδ : 0 < δ) (hR : 1 ≤ R) : DifferentiableOn ℂ (bpSeries f) ({s | δ < s.re} ∩ Metric.ball 0 R)**Bounded partial sums give a holomorphic by-parts series on a box**: the Weierstrass
`M`-test packaged from `summable_bpSeries_boxBound`, `differentiableOn_bpSeries_term`, and
`norm_bpSeries_term_le_boxBound`.  A box is used because no summable bound is uniform on the
whole half-plane `{0 < s.re}`; `differentiableOn_bpSeries` glues the boxes together.  hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C hδ0 < δ hR1 ≤ R) s₀ℂ hs₀Vs₀ ∈ {s | δ < s.re} ∩ Metric.ball 0 R).differentiableAtDifferentiableWithinAt.differentiableAt.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
  {f : E → F} {x : E} {s : Set E} (h : DifferentiableWithinAt 𝕜 f s x) (hs : s ∈ nhds x) : DifferentiableAt 𝕜 f x
    (hVopenIsOpen ({s | δ < s.re} ∩ Metric.ball 0 R).mem_nhdsIsOpen.mem_nhds.{u} {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : s ∈ nhds x hs₀Vs₀ ∈ {s | δ < s.re} ∩ Metric.ball 0 R)).differentiableWithinAtDifferentiableAt.differentiableWithinAt.{u_1, u_2, u_3} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2}
  [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
  {f : E → F} {x : E} {s : Set E} (h : DifferentiableAt 𝕜 f x) : DifferentiableWithinAt 𝕜 f s x

≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [norm_mul, norm_cpow_neg_sub_add_one_eq hσ hn]
  exact`exact e` closes the main goal if its target type matches that of `e`.
 mul_le_mul_of_nonneg_right (hC n)
    (Real.natCast_rpow_neg_sub_add_one_nonneg hσ hn)

≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hC0 : 0 ≤ C := (norm_nonneg _).trans (hC 0)
  set`set a := t with h` is a variant of `let a := t`. It adds the hypothesis `h : a = t` to
the local context and replaces `t` with `a` everywhere it can.

`set a := t with ← h` will add `h : t = a` instead.

`set! a := t with h` does not do any replacing.

```lean
example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
  set y := x with ← h2
  sorry
/-
x : Nat
y : Nat := x
h : y + y - y = 3
h2 : x = y
⊢ y + y - y = 3
-/
```
 G : ℕ → ℝ := fun n ↦ ((max n n₀ : ℕ) : ℝ) ^ (-σ) with hG
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hterm : ∀ n : ℕ,
      ‖(∑ k ∈ Finset.range (n + 1), f k) *
        ((n : ℂ) ^ (-(σ : ℂ)) - ((n : ℂ) + 1) ^ (-(σ : ℂ)))‖ ≤ C * (G n - G (n + 1)) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
    introIntroduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.

* `intro` by itself introduces one anonymous hypothesis, which can be accessed
  by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
  can be anonymized via `_`, given a type ascription, or matched against a pattern:
  ```lean
  -- ... ⊢ α × β → ...
  intro (a, b)
  -- ..., a : α, b : β ⊢ ...
  ```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
  is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
  ```lean
  intro
  | n + 1, 0 => tac
  | ...
  ```
 n
    rcases`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 lt_or_ge n n₀ with`rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 hlt | hle
    · rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [hvanish n hlt, zero_mul, norm_zero]
      haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 h1 : max n n₀ = n₀ := max_eq_right hlt.le
      haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 h2 : max (n + 1) n₀ = n₀ := max_eq_right (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.

It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.

We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.

We decompose the sides of the inequalities as linear combinations of atoms.

If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.

On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.

The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
  if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
)
      haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hzero : G n - G (n + 1) = 0 := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
        rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [hG]
        simpThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 onlyThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 [h1, h2, sub_self]
      simpThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 [hzero]
    · haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hn1 : 1 ≤ n := hn₀.trans hle
      haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hGn : G n = (n : ℝ) ^ (-σ) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
        rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [hG]
        simpThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 onlyThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 [max_eq_left hle]
      haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hGn1 : G (n + 1) = ((n : ℝ) + 1) ^ (-σ) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
        rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [hG]
        simpThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 onlyThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 [max_eq_left (show n₀ ≤ n + 1 by omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.

It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.

We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.

We decompose the sides of the inequalities as linear combinations of atoms.

If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.

On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.

The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
  if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
), Nat.cast_add, Nat.cast_one]
      rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [hGn, hGn1]
      exact`exact e` closes the main goal if its target type matches that of `e`.
 norm_bpSeries_term_le hC hσ hn1
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hG0 : G 0 = (n₀ : ℝ) ^ (-σ) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
    rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [hG]
    simpThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 onlyThe `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 [Nat.zero_max]
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hGN : 0 ≤ G N := Real.rpow_nonneg (Nat.cast_nonneg _) _
  calcStep-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 ∑ n ∈ Finset.range N,
        ‖(∑ k ∈ Finset.range (n + 1), f k) *
          ((n : ℂ) ^ (-(σ : ℂ)) - ((n : ℂ) + 1) ^ (-(σ : ℂ)))‖
      ≤ ∑ n ∈ Finset.range N, C * (G n - G (n + 1)) :=
        Finset.sum_le_sum fun n _ ↦ hterm n
    _ = C * (G 0 - G N) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [← Finset.mul_sum, Finset.sum_range_sub' G N]
    _ ≤ C * (n₀ : ℝ) ^ (-σ) := by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
        rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [← hG0]
        exact`exact e` closes the main goal if its target type matches that of `e`.
 mul_le_mul_of_nonneg_left (sub_le_self _ hGN) hC0

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hnormsumSummable fun n => ‖(∑ k ∈ Finset.range (n + 1), f k) * (↑n ^ (-↑σ) - (↑n + 1) ^ (-↑σ))‖ : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  fun nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 ↦
      ‖(∑ kℕ ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.  (nℕ + 1ℕ), fℕ → ℂ kℕ) *
        ((nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(σℝ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )) - ((nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) + 1ℂ) ^ (-(σℝ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )))‖ :=
    summable_of_sum_range_lesummable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) :
  Summable f (fun nℕ ↦ norm_nonnegnorm_nonneg.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖ _)
      (fun Nℕ ↦ sum_range_norm_bpSeries_lesum_range_norm_bpSeries_le {f : ℕ → ℂ} {C : ℝ} (hC : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C) {n₀ : ℕ}
  (hn₀ : 1 ≤ n₀) (hvanish : ∀ n < n₀, ∑ k ∈ Finset.range (n + 1), f k = 0) {σ : ℝ} (hσ : 0 ≤ σ) (N : ℕ) :
  ∑ n ∈ Finset.range N, ‖(∑ k ∈ Finset.range (n + 1), f k) * (↑n ^ (-↑σ) - (↑n + 1) ^ (-↑σ))‖ ≤ C * ↑n₀ ^ (-σ)**Telescoping majorant**: if the partial sums of `f` are bounded by `C` and vanish below
`n₀ ≥ 1`, then every partial sum of `∑ ‖by-parts term‖` on the real axis is at most
`C · n₀ ^ (-σ)`.  The nonnegative real increments telescope from `n₀` (the earlier terms
vanish), so the internal majorant `n ↦ (max n n₀) ^ (-σ)` collapses to `n₀ ^ (-σ)`.  hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C hn₀1 ≤ n₀ hvanish∀ n < n₀, ∑ k ∈ Finset.range (n + 1), f k = 0 hσ0 ≤ σ Nℕ)
  calcStep-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 ‖bpSeriesbpSeries (f : ℕ → ℂ) (s : ℂ) : ℂThe **by-parts series** attached to `f : ℕ → ℂ`:

`bpSeries f s = ∑' n, (∑ k ∈ Finset.range (n + 1), f k) * ((n : ℂ) ^ (-s) - ((n : ℂ) + 1) ^ (-s))`.

If the partial sums `∑ k ∈ Finset.range (n + 1), f k = ∑_{k ≤ n} f k` are bounded, this
series converges and is holomorphic on `{s | 0 < s.re}` (`differentiableOn_bpSeries`) and it
agrees with the Dirichlet series `∑' n, f n * (n : ℂ) ^ (-s)` for `1 < s.re`
(`tsum_mul_cpow_neg_eq_bpSeries`): it is the analytic continuation of that Dirichlet series
to the right half-plane.  This is the analytic-continuation object `Ã` of the proof.  fℕ → ℂ σℝ‖
      ≤ ∑' nℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
, ‖(∑ kℕ ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.  (nℕ + 1ℕ), fℕ → ℂ kℕ) *
          ((nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(σℝ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )) - ((nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) + 1ℂ) ^ (-(σℝ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )))‖ :=
        norm_tsum_le_tsum_normnorm_tsum_le_tsum_norm.{u_1, u_3} {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] {f : ι → E}
  (hf : Summable fun i => ‖f i‖) : ‖∑' (i : ι), f i‖ ≤ ∑' (i : ι), ‖f i‖If `∑' i, ‖f i‖` is summable, then `‖∑' i, f i‖ ≤ (∑' i, ‖f i‖)`. Note that we do not assume
that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space.  hnormsumSummable fun n => ‖(∑ k ∈ Finset.range (n + 1), f k) * (↑n ^ (-↑σ) - (↑n + 1) ^ (-↑σ))‖
    _ ≤ Cℝ * (n₀ℕ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) ^ (-σℝ) :=
        Real.tsum_le_of_sum_range_leReal.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n)
  (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) : ∑' (n : ℕ), f n ≤ c (fun nℕ ↦ norm_nonnegnorm_nonneg.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖ _)
          (fun Nℕ ↦ sum_range_norm_bpSeries_lesum_range_norm_bpSeries_le {f : ℕ → ℂ} {C : ℝ} (hC : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C) {n₀ : ℕ}
  (hn₀ : 1 ≤ n₀) (hvanish : ∀ n < n₀, ∑ k ∈ Finset.range (n + 1), f k = 0) {σ : ℝ} (hσ : 0 ≤ σ) (N : ℕ) :
  ∑ n ∈ Finset.range N, ‖(∑ k ∈ Finset.range (n + 1), f k) * (↑n ^ (-↑σ) - (↑n + 1) ^ (-↑σ))‖ ≤ C * ↑n₀ ^ (-σ)**Telescoping majorant**: if the partial sums of `f` are bounded by `C` and vanish below
`n₀ ≥ 1`, then every partial sum of `∑ ‖by-parts term‖` on the real axis is at most
`C · n₀ ^ (-σ)`.  The nonnegative real increments telescope from `n₀` (the earlier terms
vanish), so the internal majorant `n ↦ (max n n₀) ^ (-σ)` collapses to `n₀ ^ (-σ)`.  hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C hn₀1 ≤ n₀ hvanish∀ n < n₀, ∑ k ∈ Finset.range (n + 1), f k = 0 hσ0 ≤ σ Nℕ)

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 hC00 ≤ C : 0ℝ ≤ Cℝ := (norm_nonnegnorm_nonneg.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖ _).transLE.le.trans.{u_1} {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c**Alias** of `le_trans`. (hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C 0ℕ)
  refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
 (norm_bpSeries_lenorm_bpSeries_le {f : ℕ → ℂ} {C : ℝ} (hC : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C) {n₀ : ℕ} (hn₀ : 1 ≤ n₀)
  (hvanish : ∀ n < n₀, ∑ k ∈ Finset.range (n + 1), f k = 0) {σ : ℝ} (hσ : 0 ≤ σ) : ‖bpSeries f ↑σ‖ ≤ C * ↑n₀ ^ (-σ)**Real-segment bound** (real-axis telescoping): if the partial sums of `f`
are bounded by `C` and vanish for `n < n₀` (with `1 ≤ n₀`), then for real `σ ≥ 0`

`‖bpSeries f σ‖ ≤ C * (n₀ : ℝ) ^ (-σ)`.

The by-parts series converges absolutely (`sum_range_norm_bpSeries_le` bounds its partial sums)
and its norm is at most the telescoping majorant `C · n₀ ^ (-σ)`.  (For the race-sum
application: partial sums over `k ≤ 0` and `k ≤ 1` vanish since there are no primes below `2`,
so `n₀ = 2` and the bound is `C * 2 ^ (-σ)`.)  hC∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), f k‖ ≤ C hn₀1 ≤ n₀ hvanish∀ n < n₀, ∑ k ∈ Finset.range (n + 1), f k = 0 hσ0 ≤ σ).transLE.le.trans.{u_1} {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c**Alias** of `le_trans`. ?_
  calcStep-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 Cℝ * (n₀ℕ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) ^ (-σℝ) ≤ Cℝ * 1ℝ :=
        mul_le_mul_of_nonneg_leftmul_le_mul_of_nonneg_left.{u_1} {α : Type u_1} [Mul α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (hbc : b ≤ c)
  (ha : 0 ≤ a) : a * b ≤ a * c
          (Real.rpow_le_one_of_one_le_of_nonposReal.rpow_le_one_of_one_le_of_nonpos {x z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) : x ^ z ≤ 1 (Nat.one_le_castNat.one_le_cast.{u_1} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α]
  [CharZero α] {n : ℕ} : 1 ≤ ↑n ↔ 1 ≤ n.2Iff.mpr {a b : Prop} (self : a ↔ b) : b → aModus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`.  hn₀1 ≤ n₀) (neg_nonposneg_nonpos.{u} {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] {a : α} : -a ≤ 0 ↔ 0 ≤ a**Alias** of `Left.neg_nonpos_iff`.

---

Uses `left` co(ntra)variant. .2Iff.mpr {a b : Prop} (self : a ↔ b) : b → aModus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`.  hσ0 ≤ σ))
          hC00 ≤ C
    _ = Cℝ := mul_onemul_one.{u} {M : Type u} [MulOneClass M] (a : M) : a * 1 = a Cℝ

≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
 squeeze_zero_norm (a := fun N : ℕ ↦ C * (N : ℝ) ^ (-s.re)) (fun N ↦ ?_) ?_
  · rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [norm_mul,
      Complex.norm_natCast_cpow_of_re_ne_zero N
        (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [Complex.neg_re]; exact`exact e` closes the main goal if its target type matches that of `e`.
 neg_ne_zero.2 hs.ne'),
      Complex.neg_re]
    exact`exact e` closes the main goal if its target type matches that of `e`.
 mul_le_mul_of_nonneg_right (hC N) (Real.rpow_nonneg (Nat.cast_nonneg N) _)
  · haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
  hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `have` term.

## Properties and relations

* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
  The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
    Consider using the equivalent `let +nondep` to indicate the intent.

 h := ((tendsto_rpow_neg_atTop hs).comp
      (tendsto_natCast_atTop_atTop (R := ℝ))).const_mul C
    rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [mul_zero] atLocation specifications are used by many tactics that can operate on either the
hypotheses or the goal. It can have one of the forms:
* 'empty' is not actually present in this syntax, but most tactics use
  `(location)?` matchers. It means to target the goal only.
* `at h₁ ... hₙ`: target the hypotheses `h₁`, ..., `hₙ`
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
 h
    exact`exact e` closes the main goal if its target type matches that of `e`.
 h