⟲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.

 h1Summable fun p => χ ↑↑p * ↑↑p ^ (-s) : 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 pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers  ↦ χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)) :=
    summable_layerA_termA362583.summable_layerA_term {s : ℂ} (hs : 1 < s.re) : Summable fun p => χ ↑↑p * ↑↑p ^ (-s)Summability of the `layerA` integrand for `Re s > 1`.  hs1 < 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.

 h2Summable fun p => χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2 : 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 pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers  ↦ χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ) :=
    (summable_norm_term_twoA362583.summable_norm_term_two {s : ℂ} (hs : 1 / 2 < s.re) : Summable fun p => ‖χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2‖Absolute summability of the `k = 2` terms for `Re s > 1/2`
(domination by `p^(-2 Re s)`).  (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.
)).of_normSummable.of_norm.{u_1, u_3} {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E}
  (hf : Summable fun a => ‖f a‖) : Summable f
  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.

 h3Summable fun p => tp p s : 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 pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers  ↦ tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ) := summable_tpA362583.summable_tp {s : ℂ} (hs : 1 / 2 ≤ s.re) : Summable fun p => tp p sPlain summability of the `layerT` integrand on `Re s ≥ 1/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.
)
  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
 ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , -Complex.logComplex.log (x : ℂ) : ℂInverse of the `exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
`log 0 = 0`  (1ℂ - χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ))
      = ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , (χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)
          + χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ + tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ) :=
        tsum_congrtsum_congr.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β}
  {f g : β → α} (hfg : ∀ (b : β), f b = g b) : ∑'[L] (b : β), f b = ∑'[L] (b : β), g b fun pNat.Primes ↦ neg_log_splitA362583.neg_log_split (p : Nat.Primes) {s : ℂ} (hs : 1 < s.re) :
  -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = χ ↑↑p * ↑↑p ^ (-s) + χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2 + tp p s**Per-prime split**: for `Re s > 1`,
`-log(1 - χ(p) p^(-s)) = χ(p) p^(-s) + χ(p)² p^(-2s)/2 + t_p(s)`.
Proof: peel three terms off the log series with `Summable.sum_add_tsum_nat_add 3`
+ `Finset.sum_range_succ`; the `k = 0` term is `0`, the tail is definitionally
`tp p s`.  No rearrangement is involved.  pNat.Primes hs1 < s.re
    _ = (∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , (χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)
          + χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ))
          + ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes sℂ := (h1Summable fun p => χ ↑↑p * ↑↑p ^ (-s).addSummable.add.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [ContinuousAdd α] (hf : Summable f L) (hg : Summable g L) : Summable (fun b => f b + g b) L h2Summable fun p => χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2).tsum_addSummable.tsum_add.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) :
  ∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b h3Summable fun p => tp p s
    _ = ((∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ))
          + ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  ((pNat.Primes : ℕ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.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) ^ 2ℕ * ((pNat.Primes : ℕ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.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-(2ℂ * sℂ)) / 2ℂ)
          + ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`).  pNat.Primes 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.
 [h1Summable fun p => χ ↑↑p * ↑↑p ^ (-s).tsum_addSummable.tsum_add.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) :
  ∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b h2Summable fun p => χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2]
    _ = layerAA362583.layerA (s : ℂ) : ℂThe `k = 1` layer `A(s) = Σ_p χ(p) p^(-s)`.  sℂ + layerBA362583.layerB (s : ℂ) : ℂThe `k = 2` layer `B(s) = (1/2) Σ_{p odd} p^(-2s)`, with an `if`-mask at
`p = 2` (`χ(2)² = 0`, `χ(p)² = 1` for odd `p`; see `χ_sq_eq_ite`,
`tsum_term_two_eq_layerB`).  Exponent convention: `-(2 * s)`.  sℂ + layerTA362583.layerT (s : ℂ) : ℂThe `k ≥ 3` layer `T(s) = Σ_p t_p(s)`.  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.
 [tsum_term_two_eq_layerBA362583.tsum_term_two_eq_layerB (s : ℂ) : ∑' (p : Nat.Primes), χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)) / 2 = layerB sSumming the `k = 2` terms over primes gives exactly `layerB` (via
`χ_sq_eq_ite`; unconditional). ]; rflThis tactic applies to a goal whose target has the form `x ~ x`,
where `~` is equality, heterogeneous equality or any relation that
has a reflexivity lemma tagged with the attribute @[refl].

⟲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.
 [← tsum_neg_log_eq_layersA362583.tsum_neg_log_eq_layers {s : ℂ} (hs : 1 < s.re) :
  ∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = layerA s + layerB s + layerT s**Per-`p` split summed over primes**: for `Re s > 1`,
`Σ_p -log(1 - χ(p) p^(-s)) = A(s) + B(s) + T(s)`.
Proof: rewrite each term with the per-prime split `neg_log_split`, then split the sum
by linearity of three absolutely convergent series (`Summable.tsum_add` twice) and
identify the `k = 2` piece as `layerB` (`tsum_term_two_eq_layerB`).
No double-sum rearrangement is involved.  hs1 < s.re, DirichletCharacter.LFunction_eq_LSeriesDirichletCharacter.LFunction_eq_LSeries {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
  DirichletCharacter.LFunction χ s = LSeries (fun x => χ ↑x) sFor `1 < re s` the L-function of a Dirichlet character agrees with the sum of the naive Dirichlet
series.
 χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  hs1 < s.re]
  exact`exact e` closes the main goal if its target type matches that of `e`.
 DirichletCharacter.LSeries_eulerProduct_exp_logDirichletCharacter.LSeries_eulerProduct_exp_log {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
  Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = LSeries (fun n => χ ↑n) sA variant of the Euler product for Dirichlet L-series.  χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  hs1 < s.re

⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. 
  unfold* `unfold id` unfolds all occurrences of definition `id` in the target.
* `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
* `unfold id at h` unfolds at the hypothesis `h`.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to `delta`.
For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively.
 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`). 
  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [raceSum_eq_sum_raceKernelA362583.raceSum_eq_sum_raceKernel (N : ℕ) : raceSum N = ∑ p ∈ Finset.range (N + 1) with Nat.Prime p, raceKernel p`raceSum` is the sum of `raceKernel` over primes `≤ N` (definitional). , ← Finset.sum_filterFinset.sum_filter.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (p : ι → Prop)
  [DecidablePred p] (f : ι → M) : ∑ a ∈ s with p a, f a = ∑ a ∈ s, if p a then f a else 0]
  push_cast`push_cast` rewrites the goal to move certain coercions (*casts*) inward, toward the leaf nodes.
This uses `norm_cast` lemmas in the forward direction.
For example, `↑(a + b)` will be written to `↑a + ↑b`.
- `push_cast` moves casts inward in the goal.
- `push_cast at h` moves casts inward in the hypothesis `h`.
It can be used with extra simp lemmas with, for example, `push_cast [Int.add_zero]`.

Example:
```lean
example (a b : Nat)
    (h1 : ((a + b : Nat) : Int) = 10)
    (h2 : ((a + b + 0 : Nat) : Int) = 10) :
    ((a + b : Nat) : Int) = 10 := by
  /-
  h1 : ↑(a + b) = 10
  h2 : ↑(a + b + 0) = 10
  ⊢ ↑(a + b) = 10
  -/
  push_cast
  /- Now
  ⊢ ↑a + ↑b = 10
  -/
  push_cast at h1
  push_cast [Int.add_zero] at h2
  /- Now
  h1 h2 : ↑a + ↑b = 10
  -/
  exact h1
```

See also `norm_cast`.

  rflThis tactic applies to a goal whose target has the form `x ~ x`,
where `~` is equality, heterogeneous equality or any relation that
has a reflexivity lemma tagged with the attribute @[refl].

⟲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.

 h∑' (x : ↑{n | Nat.Prime n}), χ ↑↑x * ↑↑x ^ (-s) = ∑' (x : ℕ), {n | Nat.Prime n}.indicator (fun n => χ ↑n * ↑n ^ (-s)) x := tsum_subtypetsum_subtype.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Set β) (f : β → α) :
  ∑' (x : ↑s), f ↑x = ∑' (x : β), s.indicator f x {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.
 | nℕ.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number. }
    (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.
 ↦ χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  (nℕ : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * (nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ))
  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
 layerAA362583.layerA (s : ℂ) : ℂThe `k = 1` layer `A(s) = Σ_p χ(p) p^(-s)`.  sℂ
      = ∑' 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.
, Set.indicatorSet.indicator.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (x : α) : M`Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  {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.
 | nℕ.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number. }
          (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.
 ↦ χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`.  (nℕ : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  4ℕ) * (nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)) nℕ := h∑' (x : ↑{n | Nat.Prime n}), χ ↑↑x * ↑↑x ^ (-s) = ∑' (x : ℕ), {n | Nat.Prime n}.indicator (fun n => χ ↑n * ↑n ^ (-s)) x
    _ = ∑' 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.
, 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`).  nℕ * (nℕ : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ) := 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.
 tsum_congrtsum_congr.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β}
  {f g : β → α} (hfg : ∀ (b : β), f b = g b) : ∑'[L] (b : β), f b = ∑'[L] (b : β), g b fun nℕ ↦ ?_
        rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [Set.indicator_applySet.indicator_apply.{u_1, u_3} {α : Type u_1} {M : Type u_3} [Zero M] (s : Set α) (f : α → M) (a : α)
  [Decidable (a ∈ s)] : s.indicator f a = if a ∈ s then f a else 0]
        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.
 [Set.mem_setOf_eqSet.mem_setOf_eq.{u} {α : Type u} {x : α} {p : α → Prop} : (x ∈ {y | p y}) = p x]
        unfold* `unfold id` unfolds all occurrences of definition `id` in the target.
* `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
* `unfold id at h` unfolds at the hypothesis `h`.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to `delta`.
For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively.
 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`). 
        by_cases`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
 hnNat.Prime n : nℕ.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number. 
        · rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [if_posif_pos.{u} {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (if c then t else e) = t hnNat.Prime n, if_posif_pos.{u} {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (if c then t else e) = t hnNat.Prime n, χ_natCast_eq_kernelA362583.χ_natCast_eq_kernel (n : ℕ) : χ ↑n = ↑(raceKernel n)Elementary bridge: on natural casts, `χ` is `raceKernel` (the integrand of
`raceSum`), connecting the analytic layer to `raceSum`. ]
        · rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [if_negif_neg.{u} {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (if c then t else e) = e hn¬Nat.Prime n, if_negif_neg.{u} {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (if c then t else e) = e hn¬Nat.Prime n, zero_mulMulZeroClass.zero_mul.{u} {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀) : 0 * a = 0Zero is a left absorbing element for multiplication ]