A362583

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

 hz1‖χ ↑↑p * ↑↑p ^ (-s)‖ < 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ℂ)‖ < 1ℝ :=
    lt_of_le_of_ltlt_of_le_of_lt.{u_1} {α : Type u_1} [Preorder α] {a b c : α} (hab : a ≤ b) (hbc : b < c) : a < c (norm_χ_mul_cpow_le_halfA362583.norm_χ_mul_cpow_le_half (p : Nat.Primes) {s : ℂ} (hs : 1 ≤ s.re) : ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ 1 / 2`‖χ(p) p^(-s)‖ ≤ 1/2` on `Re s ≥ 1` (the domain of the per-prime split).  pNat.Primes hs1 < s.re.leLT.lt.le.{u_1} {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) : a ≤ b**Alias** of `le_of_lt`.) (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.  norm_num`norm_num` normalizes numerical expressions in the goal. By default, it supports the operations
`+` `-` `*` `/` `⁻¹` `^` and `%` over types with (at least) an `AddMonoidWithOne` instance, such as
`ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`. In addition to evaluating numerical expressions, `norm_num` will use `simp`
to simplify the goal. If the goal has the form `A = B`, `A ≠ B`, `A < B` or `A ≤ B`, where `A` and
`B` are numerical expressions, `norm_num` will try to close it. It also has a relatively simple
primality prover (available if you import `Mathlib.Tactic.NormNum.Prime`).

This tactic is extensible. Extensions can allow `norm_num` to evaluate more kinds of expressions, or
to prove more kinds of propositions (such as, primality of natural numbers). See the `@[norm_num]`
attribute for further information on extending `norm_num`.

* `norm_num at l` normalizes at location(s) `l`.
* `norm_num [h1, ...]` adds the arguments `h1, ...` to the `simp` set in addition to the default
  `simp` set. All options for `simp` arguments are supported, in particular `←`, `↑` and `↓`.
* `norm_num only` does not use the default `simp` set for simplification. `norm_num only [h1, ...]`
  uses only the arguments `h1, ...` in addition to the routines tagged `@[norm_num]`.
  `norm_num only` still performs post-processing steps, like `simp only`, use `norm_num1` if you
  exclusively want to normalize numerical expressions.
* `norm_num (config := cfg)` uses `cfg` as configuration for `simp` calls (see the `simp` tactic for
  further details).

Examples:
```lean
example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num
```
)
  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.

 hHasSum (fun k => (χ ↑↑p * ↑↑p ^ (-s)) ^ k / ↑k) (-Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) := hasSum_neg_log_one_subA362583.hasSum_neg_log_one_sub {z : ℂ} (hz : ‖z‖ < 1) : HasSum (fun k => z ^ k / ↑k) (-Complex.log (1 - z))`-log(1-z) = Σ_{k≥1} z^k/k` in `HasSum` form.  The `k = 0` term is `0`
(Lean's `z^0/0 = 0`).  Thin wrapper around `Complex.hasSum_taylorSeries_neg_log`;
the branch of `Complex.log` is pinned inside Mathlib's proof, so no separate
exp-inversion argument is needed.  hz1‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [← hHasSum (fun k => (χ ↑↑p * ↑↑p ^ (-s)) ^ k / ↑k) (-Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))).tsum_eqHasSum.tsum_eq.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {a : α} [T2Space α] [L.NeBot] (ha : HasSum f a L) : ∑'[L] (b : β), f b = a, ← hHasSum (fun k => (χ ↑↑p * ↑↑p ^ (-s)) ^ k / ↑k) (-Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))).summableHasSum.summable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {a : α} (h : HasSum f a L) : Summable f L.sum_add_tsum_nat_addSummable.sum_add_tsum_nat_add.{u_2} {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G]
  [T2Space G] {f : ℕ → G} (k : ℕ) (h : Summable f) : ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i 3ℕ, Finset.sum_range_succFinset.sum_range_succ.{u_4} {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) :
  ∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n,
    Finset.sum_range_succFinset.sum_range_succ.{u_4} {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) :
  ∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n, Finset.sum_range_oneFinset.sum_range_one.{u_4} {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) : ∑ k ∈ Finset.range 1, f k = f 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.

 h2(χ ↑↑p * ↑↑p ^ (-s)) ^ 2 = χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * 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ℕ) * ((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ℂ)) ^ 2ℕ
      = χ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ℂ)) := 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.
 [mul_powmul_pow.{u_4} {M : Type u_4} [CommMonoid M] (a b : M) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n, ← Complex.cpow_nat_mulComplex.cpow_nat_mul (x : ℂ) (n : ℕ) (y : ℂ) : x ^ (↑n * y) = (x ^ y) ^ n]
    congrApply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ f as ≍ f bs`.
The optional parameter is the depth of the recursive applications.
This is useful when `congr` is too aggressive in breaking down the goal.
For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
`congr` produces the goals `⊢ x = y` and `⊢ y = x`,
while `congr 2` produces the intended `⊢ x + y = y + x`.
 2
    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`.

    ring`ring` solves equations in *commutative* (semi)rings, allowing for variables in the
exponent. If the goal is not appropriate for `ring` (e.g. not an equality) `ring_nf` will be
suggested. See also `ring1`, which fails if the goal is not an equality.

* `ring!` will use a more aggressive reducibility setting to determine equality of atoms.

Examples:
```
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf
```

  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.

 htail∑' (k : ℕ), (χ ↑↑p * ↑↑p ^ (-s)) ^ (k + 3) / ↑(k + 3) = tp p s : ∑' kℕ : ℕ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 `ℂ`.  ((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ℂ)) ^ (kℕ + 3ℕ)
      / ((kℕ + 3ℕ : ℕ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`. ) = 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ℂ := rflrfl.{u} {α : Sort u} {a : α} : a = a`rfl : a = a` is the unique constructor of the equality type. This is the
same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although
the statement of the theorem is `a = a`, Lean will allow anything that is
definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in
Lean by `rfl`, because both sides are the same up to definitional equality.

  rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 [h2(χ ↑↑p * ↑↑p ^ (-s)) ^ 2 = χ ↑↑p ^ 2 * ↑↑p ^ (-(2 * s)), htail∑' (k : ℕ), (χ ↑↑p * ↑↑p ^ (-s)) ^ (k + 3) / ↑(k + 3) = tp p s]
  norm_num`norm_num` normalizes numerical expressions in the goal. By default, it supports the operations
`+` `-` `*` `/` `⁻¹` `^` and `%` over types with (at least) an `AddMonoidWithOne` instance, such as
`ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`. In addition to evaluating numerical expressions, `norm_num` will use `simp`
to simplify the goal. If the goal has the form `A = B`, `A ≠ B`, `A < B` or `A ≤ B`, where `A` and
`B` are numerical expressions, `norm_num` will try to close it. It also has a relatively simple
primality prover (available if you import `Mathlib.Tactic.NormNum.Prime`).

This tactic is extensible. Extensions can allow `norm_num` to evaluate more kinds of expressions, or
to prove more kinds of propositions (such as, primality of natural numbers). See the `@[norm_num]`
attribute for further information on extending `norm_num`.

* `norm_num at l` normalizes at location(s) `l`.
* `norm_num [h1, ...]` adds the arguments `h1, ...` to the `simp` set in addition to the default
  `simp` set. All options for `simp` arguments are supported, in particular `←`, `↑` and `↓`.
* `norm_num only` does not use the default `simp` set for simplification. `norm_num only [h1, ...]`
  uses only the arguments `h1, ...` in addition to the routines tagged `@[norm_num]`.
  `norm_num only` still performs post-processing steps, like `simp only`, use `norm_num1` if you
  exclusively want to normalize numerical expressions.
* `norm_num (config := cfg)` uses `cfg` as configuration for `simp` calls (see the `simp` tactic for
  further details).

Examples:
```lean
example : 43 ≤ 74 + (33 : ℤ) := by norm_num
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num
```