mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1) ≤
    span A (Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff))

Tactic:
rw [Submodule.span_le]

Goal state after:
case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1) ⊆
    ↑(span A (Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff)))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff)) ≤
    span A (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1)

Tactic:
rw [Submodule.span_le]

Goal state after:
case a
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule A[x] = span A (Set.range ⇑pb.basis)
⊢ Set.range ((fun a ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff) ⊆
    ↑(span A (Set.range fun x_1 ↦ ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2
⊢ 3 < (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Goal state before:
pp: case h
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 3 < π

Tactic:
exact pi_gt_three

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
this✝ : Fact (Nat.Prime 5)
this : (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2
⊢ 125 < (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Goal state before:
pp: case hab
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {5} ℚ K
this : Fact (Nat.Prime 5)
⊢ 3 < π

Tactic:
exact pi_gt_three

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : w.IsReal
⊢ 1 ≤ ↑1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : ¬w.IsReal
⊢ 1 ≤ ↑2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : w.IsReal
⊢ 0 ≤ ↑1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x✝ : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x✝)‖ ≤ r
w : InfinitePlace K
x : ℝ
hx : 0 ≤ x
h✝ : ¬w.IsReal
⊢ 0 ≤ ↑2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:

Tactic:
(λ ^ 2 : K) = η ^ 2 + η + 1 - 3 * η := by
        simp only [IsUnit.unit_spec]; ring
  _ = 0 - 3 * η := by simpa using hζ.isRoot_cyclotomic (by decide)
  _ = -3 * η := by ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
h✝ : w₀.IsReal
⊢ -↑1 < 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
h✝ : ¬w₀.IsReal
⊢ -↑2 < 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
h✝ : (↑x).IsReal
⊢ 0 < ↑1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
h✝ : ¬(↑x).IsReal
⊢ 0 < ↑2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
· rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
· have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
    have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x := by
      rw [isSquare_iff_exists_sq x]
      simp_rw [eq_comm]
    rw [hs]
    rwa [card p] at h₀

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: ⊢ StrictMono fermatNumber

Tactic:
intro m n

Goal state after:
m n : ℕ
⊢ m < n → m.fermatNumber < n.fermatNumber
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
⊢ legendreSym q ↑p = -legendreSym p ↑q

Tactic:
let nop := @neg_one_pow_div_two_of_three_mod_four
  rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul] <;>
  rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : emultiplicity λ (S'.a + ↑η ^ 2 * S'.b) < ↑2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False

Tactic:
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + ↑η * S'.b) < 2
h3 : multiplicity λ (S'.a + ↑η ^ 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + ↑η * S'.b)
h3' : FiniteMultiplicity λ (S'.a + ↑η ^ 2 * S'.b)
⊢ False
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
gt : m < n
⊢ m ∈ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})

Tactic:
simpa using .inr ⟨gt, hm⟩

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case calc_1
n : ℕ
⊢ Real.log ↑(n + 1) = ∫ (x : ℝ) in ↑1..↑(n + 1), x⁻¹

pp: case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in ↑1..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹

pp: case calc_3
n : ℕ
⊢ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹ = ↑(harmonic n)

Tactic:
· rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]), div_one]

Goal state after:
case calc_2
n : ℕ
⊢ ∫ (x : ℝ) in ↑1..↑(n + 1), x⁻¹ ≤ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹

case calc_3
n : ℕ
⊢ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹ = ↑(harmonic n)
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case e'_3.e'_5
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 = 2 - 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
sub_div,

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ((↑n + 1) ^ (-2 + 1) / (-2 + 1) - ↑n ^ (-2 + 1) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -2 + 1 = -1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, v (x i)

Tactic:
ext1 v

Goal state after:
case inr.e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
v : AbsoluteValue K ℝ
⊢ ⨆ i, v (Sum.elim x 0 i) = ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, ↑v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, ↑v (x i)

Tactic:
ext1 v

Goal state after:
case inr.e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (Sum.elim x 0 i) = ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x - ↑n) / x ^ (s + 1) = x ^ (-s) - ↑n * x ^ (-(s + 1))

Tactic:
sub_div,

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ x / x ^ (s + 1) - ↑n / x ^ (s + 1) = x ^ (-s) - ↑n * x ^ (-(s + 1))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (y i_1)

Tactic:
ext1 v

Goal state after:
case e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : AbsoluteValue K ℝ
⊢ ⨆ i, v (x i.1 * y i.2) = (⨆ i, v (x i)) * ⨆ i, v (y i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, ↑v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, ↑i (x i_1)) * ⨆ i_1, ↑i (y i_1)

Tactic:
ext1 v

Goal state after:
case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (x i.1 * y i.2) = (⨆ i, ↑v (x i)) * ⨆ i, ↑v (y i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₁
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (constantCoeff (p i))) archAbsVal).prod ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod

Tactic:
have H (v : AbsoluteValue K ℝ) (j : ι') :
        v (constantCoeff (p j)) ≤ (AddMonoidAlgebra.coeff <| p j).sum fun _ c ↦ v c :=
      single_eval_le_sum _ v.map_zero (fun _ ↦ by positivity) _

Goal state after:
case h₁
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
H : ∀ (v : AbsoluteValue K ℝ) (j : ι'), v (constantCoeff (p j)) ≤ (p j).coeff.sum fun x c ↦ v c
⊢ (Multiset.map (fun v ↦ ⨆ i, v (constantCoeff (p i))) archAbsVal).prod ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
⊢ termSum s N =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
by
  simp only [termSum]
  conv => enter [1, 2, n]; rw [term_of_lt (by simp) hs]
  rw [Finset.sum_sub_distrib]
  congr 1
  · induction N with
    | zero => simp
    | succ N hN =>
      rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf
  · simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]
    congr 1
    induction N with
    | zero => simp
    | succ N hN =>
      simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
      congr 1
      ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ totalWeight K = ∑ v, v.mult

Tactic:
simp only [totalWeight]
  convert! sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))
  · rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
  · simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ 2 / 3 < 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ 2.7182818286 < 4 * 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 2 ∈ {1}ᶜ

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
v : ↑nonarchAbsVal
⊢ 0 ≤ (⨆ i, ↑v (x i)) ^ N

Tactic:
simp only [HH₁]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 2 ∈ {b | 1 < b.re}

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
inv_mul_le_iff₀ ?hC,

Goal state after:
case inr
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ mulHeight x ^ N ≤ ↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)

case hC
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ 0 < ↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∃ n, n ≠ 0 ∧ ↑n ≤ mulHeight₁ x ∧ IsIntegral ℤ (↑n * x)

Tactic:
by
  obtain ⟨n, hn, a, ha₁, ha₂⟩ := exists_nat_ne_zero_exists_integer_mul_eq_and_absNorm_span_eq_pow x
  refine ⟨n, hn, ?_, ha₁ ▸ a.isIntegral_coe⟩
  rw [← totalWeight_eq_finrank] at ha₂
  have hv (i : Fin 2) : (![a, n] i : K) = ![(a : K), n] i := by fin_cases i <;> rfl
  rw [← mul_div_cancel_left₀ x (mod_cast hn : (n : K) ≠ 0), ha₁, mulHeight₁_div_eq_mulHeight,
    mulHeight_eq (by simp [hn])]
  refine le_of_mul_le_mul_left ?_ (show (0 : ℝ) < n ^ (totalWeight K - 1) by positivity)
  have : n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![(a : K), n] i) = 1 := by
    simpa [ha₂, hv] using absNorm_mul_finprod_finitePlace_eq_one (show ![a, n] ≠ 0 by simp [hn])
  rw [pow_sub_one_mul (totalWeight_pos K).ne', mul_left_comm, this, mul_one,
    totalWeight_eq_sum_mult, ← prod_pow_eq_pow_sum univ]
  gcongr
  exact Finite.le_ciSup_of_le 1 <| by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : (∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)) * ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B

Tactic:
← ha,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : (∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)) * ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤
    ↑n ^ totalWeight K * ((∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)) * ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult)