mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this : IsDomain 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this✝ : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this : IsDomain 𝒪
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝ : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main :
  𝒑.inertiaDegIn (𝓞 ↥Fₘ) * 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) =
    (Pₘ.primesOver (𝓞 K)).ncard * (𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K))
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

Tactic:
← mul_assoc,

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main :
  𝒑.inertiaDegIn (𝓞 ↥Fₘ) * 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) =
    (Pₘ.primesOver (𝓞 K)).ncard * 𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K)
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
s : ℝ
⊢ ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) * s⁻¹ =
    ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) * ↑(torsionOrder K) *
        (s⁻¹ * (↑(absNorm ↑J))⁻¹) *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
← mul_assoc,

Goal state after:
case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
s : ℝ
⊢ ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) * s⁻¹ =
    ↑(Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }) * ↑(torsionOrder K) * s⁻¹ *
          (↑(absNorm ↑J))⁻¹ *
        ↑(absNorm ↑J) *
      (↑(torsionOrder K))⁻¹
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), w ↑α < 1
⊢ False

Tactic:
let w₀ := Classical.arbitrary (InfinitePlace K)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), w ↑α < 1
w₀ : InfinitePlace K := Classical.arbitrary (InfinitePlace K)
⊢ False
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

Tactic:
negPart_eq_zero.2 hsign

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ -(↑B * 0) ≤ v j * A i j
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z.appr k ∈ ↑(Finset.range (p ^ k))

Tactic:
simpa only [Finset.mem_coe, Finset.mem_range] using z.appr_lt k

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ U

Tactic:
apply hV

Goal state after:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
ht : Disjoint t (Set.Finite.toFinset ⋯)
⊢ ∏ b ∈ t, f b ∈ ↑V
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
⊢ f ↑n ≤ (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n

Tactic:
have h_ineq1 {m n : ℕ} (hm : 1 < m) (hn : 1 < n) :
      f n ≤ (m * f m / (f m - 1)) * f m ^ logb m n := by
    let d := Nat.log m n
    have hfm := one_lt_of_not_bounded notbdd hm
    calc
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * f m ^ i).sum := apply_le_sum_digits n hm
    _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
    _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
      rw [list_geom _ hfm.ne', ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
    _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
      gcongr; linarith
    _ = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d := by ring
    _ ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n := by
      gcongr
      rw [← rpow_natCast, rpow_le_rpow_left_iff hfm]
      exact natLog_le_logb n m

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
⊢ f ↑n ≤ (↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹ * f ↑m ^ logb ↑m ↑n
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * (supOfBasis K * (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))) ≤
    ↑h * (max 1 (c K) * supOfBasis K) * (↑q * (↑(finrank ℚ K) * c₂ K) * A) ^ (↑p / (↑q - ↑p))

Tactic:
← mul_assoc,

Goal state after:
case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * supOfBasis K * (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * (max 1 (c K) * supOfBasis K) * (↑q * (↑(finrank ℚ K) * c₂ K) * A) ^ (↑p / (↑q - ↑p))
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ (addChar_of_value_at_one r hr) 1 = 1 + r

Tactic:
change mahlerSeries (r ^ ·) ↑(1 : ℕ) = _

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ (mahlerSeries fun x ↦ r ^ x) ↑1 = 1 + r
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
⊢ (mahler k) ↑n = ↑(n.choose k)

Tactic:
by
  simp only [mahler_apply, Ring.choose_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0)
⊢ f = mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0

Tactic:
refine ContinuousMap.coe_injective (denseRange_natCast.equalizer
    (map_continuous f) (map_continuous _) (funext fun n ↦ ?_))

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0)
n : ℕ
⊢ (⇑f ∘ Nat.cast) n = (⇑(mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0) ∘ Nat.cast) n
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 1 < (eval (↑b) (cyclotomic (k + 1) ℤ)).natAbs

Tactic:
have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos

Goal state after:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
hb : 2 ≤ b
⊢ 1 < (eval (↑b) (cyclotomic (k + 1) ℤ)).natAbs
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ |d * (a.y * b.y)| < a.x * b.x

Tactic:
rw [← abs_of_pos ha, ← abs_of_pos hb, ← abs_mul, ← sq_lt_sq, mul_pow a.x, a.prop_x, b.prop_x, ←
    sub_pos]

Goal state after:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (1 + d * a.y ^ 2) * (1 + d * b.y ^ 2) - (d * (a.y * b.y)) ^ 2
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ ‖(Polynomial.aeval a) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ 0

Tactic:
simp [T_def, mul_div_cancel₀ _ (ne_of_gt (deriv_sq_norm_pos hnorm))]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
hx₁ : 1 < a.x
hyy : 0 ≤ (a * a₁⁻¹).y
x' : ℕ
hx' : ↑x' = (a * a₁⁻¹).x
hxx₁ : 0 < ↑x'
hxx₂ : ↑x' < a.x
n : ℕ
hn : a * a₁⁻¹ = a₁ ^ n
⊢ a = a₁ * (a₁⁻¹ * a)

Tactic:
← mul_assoc,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
hx₁ : 1 < a.x
hyy : 0 ≤ (a * a₁⁻¹).y
x' : ℕ
hx' : ↑x' = (a * a₁⁻¹).x
hxx₁ : 0 < ↑x'
hxx₂ : ↑x' < a.x
n : ℕ
hn : a * a₁⁻¹ = a₁ ^ n
⊢ a = a₁ * a₁⁻¹ * a
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: case inr
A : Type u_1
B : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : Module.IsTorsionFree A B
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : Ideal.span {x} ≠ ⊥
⊢ emultiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x})) =
    ↑(v.asIdeal.ramificationIdx' w.asIdeal * multiplicity v.asIdeal (Ideal.span {x}))

Tactic:
rw [emultiplicity_map_eq_ramificationIdx'_mul hx v.irreducible w.irreducible w.ne_bot,
    Nat.cast_mul, (FiniteMultiplicity.of_prime_left v.prime hx).emultiplicity_eq_multiplicity]

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ↑p / v ↑q = v X ^ p.natDegree / v X ^ q.natDegree

Tactic:
have hp : p ≠ 0 := by contrapose hf; simp [hf]

Goal state after:
case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp : p ≠ 0
⊢ v ↑p / v ↑q = v X ^ p.natDegree / v X ^ q.natDegree
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inr
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
hlt' : 1 < (inftyValuation K) X
⊢ v f < 1 ↔ (inftyValuation K) f < 1

Tactic:
rw [valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt hf,
      valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt' hf]

Goal state after:
case inr
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
hlt' : 1 < (inftyValuation K) X
⊢ v X ^ f.intDegree < 1 ↔ (inftyValuation K) X ^ f.intDegree < 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a
s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
d e : ℕ
hd : (d, e) ∈ l.divisorsAntidiagonal
⊢ (s.nu l)⁻¹ * (↑(μ (d, e).1) * s.nu (d, e).1) = ↑(μ (d, e).1) * (s.nu (d, e).2)⁻¹

Tactic:
obtain ⟨rfl, -⟩ : d * e = l ∧ _ := by simpa using hd

Goal state after:
case a
s : BoundingSieve
d e : ℕ
hl : Squarefree (d * e)
hnu_nonzero : s.nu (d * e) ≠ 0
hd : (d, e) ∈ (d * e).divisorsAntidiagonal
⊢ (s.nu (d * e))⁻¹ * (↑(μ (d, e).1) * s.nu (d, e).1) = ↑(μ (d, e).1) * (s.nu (d, e).2)⁻¹
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
⊢ toComplex x = toComplex y ↔ x = y

Tactic:
cases x; cases y; simp [toComplex_def₂]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this✝ :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
this : ∑ x, f (σ x) ^ 2 = ∑ x, f x ^ 2
⊢ 2 * x + 2 * y = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2

Tactic:
simpa only [← hx, ← hy, Fin.sum_univ_four, add_assoc] using! this

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide
  rw [ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hn]
  refine ⟨?_, fun H q hq => H <| Nat.dvd_of_mem_primeFactors hq⟩
  intro H
  refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)
  · exact fun _ => by simp
  · exact fun _ => by simp
  · replace hp := H _ <|
      Nat.mem_primeFactors.mpr ⟨hp, dvd_of_mul_right_dvd hpq, Squarefree.ne_zero hn⟩
    replace hq := hq (dvd_of_mul_left_dvd hpq)
    rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢
    rw [Nat.cast_mul]
    exact help p q hp hq

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑u * ↑y * (↑u * ↑y)

Tactic:
conv_rhs => tactic => norm_cast

Goal state after:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ (Quotient.mk (P ^ e)) (-z) = (Quotient.mk (P ^ e)) (a * y) - (Quotient.mk (P ^ e)) (a * y + z)

Tactic:
map_add,

Goal state after:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ (Quotient.mk (P ^ e)) (-z) = (Quotient.mk (P ^ e)) (a * y) - ((Quotient.mk (P ^ e)) (a * y) + (Quotient.mk (P ^ e)) z)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ¬↑a * ↑q - ↑b * ↑p = 0
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
a1 : |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q
⊢ a * q - ↑b * p ≠ 0

Tactic:
exact mod_cast a0

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ finrank (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P) = p.ramificationIdx' ↑P * p.inertiaDeg' ↑P

Tactic:
finrank_prime_pow_ramificationIdx,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P * finrank (R ⧸ p) (S ⧸ ↑P) = p.ramificationIdx' ↑P * p.inertiaDeg' ↑P

case hP0
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ ↑P ≠ ⊥

case he
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P ≠ 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < 1 / A

Tactic:
refine (lt_div_iff₀' hA).mpr ?_

Goal state after:
case refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
h : 1 ≤ ↑b ^ f.natDegree * (|x - ↑a / ↑b| * A)
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
⊢ 1 / A ≤ ↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|

pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
h : 1 ≤ ↑b.pred.succ ^ f.natDegree * (|x - ↑a / ↑b.pred.succ| * A)
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
⊢ 1 < b

Tactic:
← mul_assoc,

Goal state after:
case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
h : 1 ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b| * A
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
⊢ 1 / A ≤ ↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|

x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
h : 1 ≤ ↑b.pred.succ ^ f.natDegree * (|x - ↑a / ↑b.pred.succ| * A)
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
⊢ 1 < b