A362583

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  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.
 ⟨cℝ, Cℝ, hC∀ (N : ℕ), |↑(raceSum N) - c * ↑N.primeCounting| ≤ C⟩
  -- Case `c ≠ 0` (CaseNonzero.lean) forces `c = 0`, leaving the bounded-race case.
  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.

 hcc = 0 : cℝ = 0ℝ := c_eq_zero_of_raceSum_linearA362583.c_eq_zero_of_raceSum_linear {c C : ℝ} (hC : ∀ (N : ℕ), |↑(raceSum N) - c * ↑N.primeCounting| ≤ C) : c = 0**The slope is zero**: if the race sum is `c·π + O(1)`, then `c = 0`.  This is what
reduces `raceSum_not_linear` to the bounded-race case `|raceSum N| ≤ C`.

If `c ≠ 0`, the Abel bound and the boundedness of `A` on `(1, 2]` give `|c|·P(σ) ≤ C + K` for
all `σ ∈ (1, 2]`, but divergence transfer (`exists_one_lt_tsum_primes_rpow_gt`, the sole prime
input `Σ 1/p = ∞`) produces a single `σ ∈ (1, 2)` where `P(σ) > (C + K)/|c|`.  Contradiction.  hC∀ (N : ℕ), |↑(raceSum N) - c * ↑N.primeCounting| ≤ C
  subst`subst x...` substitutes each hypothesis `x` with a definition found in the local context,
then eliminates the hypothesis.
- If `x` is a local definition, then its definition is used.
- Otherwise, if there is a hypothesis of the form `x = e` or `e = x`,
  then `e` is used for the definition of `x`.

If `h : a = b`, then `subst h` may be used if either `a` or `b` unfolds to a local hypothesis.
This is similar to the `cases h` tactic.

See also: `subst_vars` for substituting all local hypotheses that have a defining equation.
 hcc = 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.

 hS∀ (N : ℕ), |↑(raceSum N)| ≤ C : ∀ 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.
, |(raceSumA362583.raceSum (N : ℕ) : ℤChebyshev race sum `S(N) = Σ_{p ≤ N} χ₄(p)`, stated elementarily as the sum of
`raceKernel` over primes `≤ N`: `+1` for primes `≡ 1 (mod 4)`, `-1` for primes
`≡ 3 (mod 4)`, `0` for `p = 2`.  The range `Finset.range (N + 1)` means primes `≤ N`,
matching the convention of `Nat.primeCounting N` (# primes `≤ N`).  Nℕ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )| ≤ Cℝ := fun Nℕ ↦ by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  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.
 usingThe arguments to the `simpa` family tactics.  hC∀ (N : ℕ), |↑(raceSum N) - 0 * ↑N.primeCounting| ≤ C 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.

 hB∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), fChi k‖ ≤ C : ∀ nℕ, ‖∑ kℕ ∈ Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`.  (nℕ + 1ℕ), fChiA362583.fChi (n : ℕ) : ℂBridge: the ℕ-indexed coefficient function of `layerA` — `raceKernel n` at
primes, `0` elsewhere.  Its partial sums are exactly `raceSum` (`sum_range_fChi`),
so `Complex.bpSeries fChi` is the by-parts continuation of `layerA`
(via `layerA_eq_tsum_fChi` + `Complex.tsum_mul_cpow_neg_eq_bpSeries`).  kℕ‖ ≤ Cℝ := norm_sum_range_fChi_leA362583.norm_sum_range_fChi_le {C : ℝ} (hS : ∀ (N : ℕ), |↑(raceSum N)| ≤ C) (n : ℕ) :
  ‖∑ k ∈ Finset.range (n + 1), fChi k‖ ≤ CUnder the bounded-race hypothesis `|S(N)| ≤ C`, the partial sums of `fChi` are
bounded by `C` in norm — they are exactly the race sums (`sum_range_fChi`).  hS∀ (N : ℕ), |↑(raceSum N)| ≤ C
  -- Continuity of `L(χ, ·)` at `1/2`: a bound `M₀` on a `δ₀`-ball.
  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.
 ⟨M₀ℝ, hM₀pos0 < M₀, δ₀ℝ, hδ₀pos0 < δ₀, hball∀ (s : ℂ), ‖s - ↑(1 / 2)‖ < δ₀ → ‖DirichletCharacter.LFunction χ s‖ < M₀⟩ := exists_norm_LFunction_lt_near_halfA362583.exists_norm_LFunction_lt_near_half :
  ∃ M₀, 0 < M₀ ∧ ∃ δ₀, 0 < δ₀ ∧ ∀ (s : ℂ), ‖s - ↑(1 / 2)‖ < δ₀ → ‖DirichletCharacter.LFunction χ s‖ < M₀`L(χ, ·)` is entire, hence continuous at `1/2`: there are `M₀ > 0` and `δ₀ > 0` with
`‖L(χ, s)‖ < M₀` for every `s` within `δ₀` of `1/2`.  No bounded-race hypothesis is used. 
  -- Divergence transfer: a single point `σ ∈ (1/2, 1/2 + δ₀)` where `layerBReal` is huge.
  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σlo1 / 2 < σ, hσhiσ < 1 / 2 + δ₀, hσBReal.log M₀ + C + cT < layerBReal σ⟩ := exists_layerBReal_gtA362583.exists_layerBReal_gt (M : ℝ) {η : ℝ} (hη : 0 < η) : ∃ σ, 1 / 2 < σ ∧ σ < 1 / 2 + η ∧ M < layerBReal σ**Divergence transfer at `s ↓ 1/2` (`layerBReal` blow-up)**: for every `M` and
`η > 0` there is a real `σ ∈ (1/2, 1/2+η)` with `layerBReal σ > M`.  Only prime
input: the divergence of `Σ 1/p`.  (Real.logReal.log (x : ℝ) : ℝThe real logarithm function, equal to the inverse of the exponential for `x > 0`,
to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
`(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
the derivative of `log` is `1/x` away from `0`.  M₀ℝ + Cℝ + cTA362583.cT : ℝExplicit uniform bound for `layerT` on `Re s ≥ 1/2`:
`cT = (4/3) Σ_p p^(-3/2)` (a crude `κ ≤ 4` version of the `κ/3 · Σ n^(-3/2)` bound). ) hδ₀pos0 < δ₀
  -- At `σ` the identity gives `‖L(χ, σ)‖ = exp (Re (contLog σ)) > M₀` …
  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.

 hGgtReal.log M₀ < (contLog ↑σ).re : Real.logReal.log (x : ℝ) : ℝThe real logarithm function, equal to the inverse of the exponential for `x > 0`,
to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
`(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
the derivative of `log` is `1/x` away from `0`.  M₀ℝ < (contLogA362583.contLog (s : ℂ) : ℂThe continued logarithm `G := Ã + B + T`, where `Ã = bpSeries fChi`
is the by-parts continuation of the `k = 1` layer and `B`, `T` are the `k = 2` and `k ≥ 3`
layers.  Under the bounded-race hypothesis it is holomorphic on `Ω = {Re s > 1/2}`
(`differentiableOn_contLog`) and `exp ∘ contLog = L(χ, ·)` there (`exp_contLog_eqOn`).  ((σℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  := 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.

 := layerBReal_sub_le_re_contLogA362583.layerBReal_sub_le_re_contLog {C : ℝ} (hB : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), fChi k‖ ≤ C) {σ : ℝ}
  (hσ : 1 / 2 < σ) : layerBReal σ - C - cT ≤ (contLog ↑σ).reUnder the bounded-race hypothesis, `Re (contLog σ)` is bounded below by
`layerBReal σ - C - cT` on `Ω`: writing
`Re (contLog σ) = Re (bpSeries fChi σ) + layerBReal σ + layerTReal σ`, the by-parts real
part is `≥ -C` (`norm_bpSeries_le_const`) and `layerTReal σ ≥ -cT` (`abs_layerTReal_le`).  hB∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), fChi k‖ ≤ C hσlo1 / 2 < σ
    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.

  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.

 hLbigM₀ < ‖DirichletCharacter.LFunction χ ↑σ‖ : M₀ℝ < ‖DirichletCharacter.LFunctionDirichletCharacter.LFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂThe unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, χ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as `LSeries χ`: they agree in the convergence range, but
`LSeries χ s` is defined to be `0` if `re s ≤ 1`.
 χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((σℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )‖ := 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_LFunction_eq_exp_re_contLogA362583.norm_LFunction_eq_exp_re_contLog {C : ℝ} (hB : ∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), fChi k‖ ≤ C) {σ : ℝ}
  (hσ : 1 / 2 < σ) : ‖DirichletCharacter.LFunction χ ↑σ‖ = Real.exp (contLog ↑σ).reUnder the bounded-race hypothesis, on `Ω` the L-function has norm `exp (Re (contLog σ))`:
for real `σ` with `1/2 < σ`, `‖L(χ, σ)‖ = Real.exp ((contLog σ).re)`, from the identity
`exp ∘ contLog = L(χ, ·)` (`exp_contLog_eqOn`).  hB∀ (n : ℕ), ‖∑ k ∈ Finset.range (n + 1), fChi k‖ ≤ C hσlo1 / 2 < σ]
    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
 M₀ℝ = Real.expReal.exp (x : ℝ) : ℝThe real exponential function, defined as the real part of the complex exponential  (Real.logReal.log (x : ℝ) : ℝThe real logarithm function, equal to the inverse of the exponential for `x > 0`,
to `log |x|` for `x < 0`, and to `0` for `0`. We use this unconventional extension to
`(-∞, 0]` as it gives the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and
the derivative of `log` is `1/x` away from `0`.  M₀ℝ) := (Real.exp_logReal.exp_log {x : ℝ} (hx : 0 < x) : Real.exp (Real.log x) = x hM₀pos0 < M₀).symmEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = aEquality is symmetric: if `a = b` then `b = a`.

Because this is in the `Eq` namespace, if you have a variable `h : a = b`,
`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)

      _ < Real.expReal.exp (x : ℝ) : ℝThe real exponential function, defined as the real part of the complex exponential  ((contLogA362583.contLog (s : ℂ) : ℂThe continued logarithm `G := Ã + B + T`, where `Ã = bpSeries fChi`
is the by-parts continuation of the `k = 1` layer and `B`, `T` are the `k = 2` and `k ≥ 3`
layers.  Under the bounded-race hypothesis it is holomorphic on `Ω = {Re s > 1/2}`
(`differentiableOn_contLog`) and `exp ∘ contLog = L(χ, ·)` there (`exp_contLog_eqOn`).  ((σℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )).reComplex.re (self : ℂ) : ℝThe real part of a complex number. ) := Real.exp_lt_expReal.exp_lt_exp {x y : ℝ} : Real.exp x < Real.exp y ↔ x < y.mprIff.mpr {a b : Prop} (self : a ↔ b) : b → aModus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`.  hGgtReal.log M₀ < (contLog ↑σ).re
  -- … but `σ` is within `δ₀` of `1/2`, so `‖L(χ, σ)‖ < M₀`.  Contradiction.
  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.

 hLsmall‖DirichletCharacter.LFunction χ ↑σ‖ < M₀ : ‖DirichletCharacter.LFunctionDirichletCharacter.LFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂThe unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, χ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as `LSeries χ`: they agree in the convergence range, but
`LSeries χ s` is defined to be `0` if `re s ≤ 1`.
 χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((σℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. )‖ < M₀ℝ := 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.
 hball∀ (s : ℂ), ‖s - ↑(1 / 2)‖ < δ₀ → ‖DirichletCharacter.LFunction χ s‖ < M₀ _ ?_
    rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [← Complex.ofReal_subComplex.ofReal_sub (r s : ℝ) : ↑(r - s) = ↑r - ↑s, Complex.norm_realComplex.norm_real (r : ℝ) : ‖↑r‖ = ‖r‖, Real.norm_eq_absReal.norm_eq_abs (r : ℝ) : ‖r‖ = |r|,
      abs_of_posabs_of_pos.{u_1} {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (h : 0 < a) : |a| = a (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.
)]
    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.

  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.