mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ P.ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
have : IsGalois ℚ K := isGalois {n} ℚ K

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsGalois ℚ K
⊢ P.ramificationIdx ℤ = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun j ↦ (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i‖ ≤
    ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.map
        (fun x ↦
          match x with
          | (a, i) => y ^ i)
        l.zipIdx).sum =
    ∑ i, y ^ ↑i

Tactic:
← Fin.sum_univ_fun_getElem

Goal state after:
T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (∑ i,
      match l.zipIdx[↑i] with
      | (a, i) => y ^ i) =
    ∑ i, y ^ ↑i
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : ∑ x_1, ∑ x_2, a' K a k x_1 x_2 u * x (x_1, x_2) = 0 (k, u)
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
sum_comm

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : ∑ y, ∑ x_1, a' K a k x_1 y u * x (x_1, y) = 0 (k, u)
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, ∑ i, (∑ l, ↑(a' K a k l i u) * ↑(x (l, i))) * (newBasis K) u
⊢ 0 = ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
sum_comm

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
⊢ 0 = ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r : K →+* ℂ
⊢ ∑ l, ∑ i, ↑(a' K a k i r l) * ↑(x (i, r)) * (newBasis K) l =
    ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
sum_comm

Goal state after:
case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r : K →+* ℂ
⊢ ∑ y, ∑ x_1, ↑(a' K a k y r x_1) * ↑(x (y, r)) * (newBasis K) x_1 =
    ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u
⊢ 0 = (a *ᵥ ξ K x) k

Tactic:
sum_comm

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
⊢ 0 = (a *ᵥ ξ K x) k
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
⊢ CauchySeq f

Tactic:
by
  suffices Tendsto (fun p : ℕ × ℕ ↦ f p.2 / f p.1) atTop (𝓝 1) by simpa [CauchySeq,
      cauchy_map_iff, prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one G, atTop_neBot]
  rw [tendsto_atTop']
  intro s hs
  obtain ⟨t, ht⟩ := is_nonarchimedean s hs
  obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b, N ≤ b → f (b + 1) / f b ∈ t := by
    simpa using! tendsto_def.mp hf t t.mem_nhds_one
  refine ⟨(N, N), ?_⟩
  rintro ⟨M, M'⟩ ⟨(hMN : N ≤ M), (hMN' : N ≤ M')⟩
  apply ht
  wlog h : M ≤ M' generalizing M M'
  · simpa [inv_div] using! t.inv_mem <| this _ _ hMN' hMN (le_of_not_ge h)
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  clear h hMN'
  induction k with
  | zero => simp
  | succ k ih => simpa using! t.mul_mem (hN _ (by lia : N ≤ M + k)) ih

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
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ HasSum (fun n ↦ mahlerTerm (a n) n) (mahlerSeries a)

Tactic:
refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum
  rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢
  simpa only [norm_mahlerTerm, Nat.cofinite_eq_atTop] using ha

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
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ x ∈ range (n + 1), ∑ x_1 ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (0 + x • 1).choose x_1 • a x_1 =
    ∑ x ∈ range (n + 1), ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (0 + k • 1).choose x • a x

Tactic:
sum_comm

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
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ ∑ y ∈ range (n + 1), ∑ x ∈ range (n + 1), ((-1) ^ (n - x) * ↑(n.choose x)) • (0 + x • 1).choose y • a y =
    ∑ x ∈ range (n + 1), ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (0 + k • 1).choose x • a x
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ : WithVal (Rat.padicValuation p)
⊢ ⋯.extend coe' ((extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯) ↑a✝) = ↑a✝

Tactic:
rw [extensionHom_coe]

Goal state after:
case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ : WithVal (Rat.padicValuation p)
⊢ ⋯.extend coe' (((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) a✝) = ↑a✝
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |↑q| - |ξ| ≤ 1

Tactic:
refine (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans ?_)

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 / ↑q.den ^ 2 ≤ 1
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]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ z' = a

Tactic:
let h := z' - a
  let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion a h
  simp only [Polynomial.eval_map_algebraMap, Polynomial.derivative_map] at hq
  have : (F.derivative.aeval a + q * h) * h = 0 := by calc
    _ = F.aeval (a + h) := by rw [hq, ha, zero_add, sq, right_distrib, mul_assoc]
    _ = _ := show F.aeval (a + (z' - a)) = 0 by simp [hz']
  have : h = 0 := by_contra fun hne ↦
    have : F.derivative.aeval a + q * h = 0 :=
      (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne
    have : F.derivative.aeval a = -q * h := by simpa using eq_neg_of_add_eq_zero_left this
    lt_irrefl ‖F.derivative.aeval a‖
      (calc
        ‖F.derivative.aeval a‖ = ‖q‖ * ‖h‖ := by simp [this]
        _ ≤ 1 * ‖h‖ := by gcongr; apply PadicInt.norm_le_one
        _ < ‖F.derivative.aeval a‖ := by simpa)
  exact eq_of_sub_eq_zero (by rw [← this])

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
⊢ StrictMono fun n ↦ (a ^ n).y

Tactic:
refine strictMono_int_of_lt_succ fun n => ?_

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
⊢ (a ^ n).y < (a ^ (n + 1)).y
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: case refine_2
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
x✝ : ↥(stabilizer Gal(L/K) P)
y z : B
left✝ : z ∈ nonZeroDivisors B
⊢ (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • (algebraMap B L) y /
      (P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • (algebraMap B L) z =
    x✝ • (algebraMap B L) y / x✝ • (algebraMap B L) z

Tactic:
subgroup_smul_def,

Goal state after:
case refine_2
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
x✝ : ↥(stabilizer Gal(L/K) P)
y z : B
left✝ : z ∈ nonZeroDivisors B
⊢ ↑((P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝) • (algebraMap B L) y /
      ↑((P.stabilizerEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝) • (algebraMap B L) z =
    ↑x✝ • (algebraMap B L) y / ↑x✝ • (algebraMap B L) z
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: case refine_2
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
E : Type u_6
inst✝¹¹ : Field E
inst✝¹⁰ : Algebra E L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(inertia G P)) E L
x✝ : ↥(inertia Gal(L/K) P)
y z : B
left✝ : z ∈ nonZeroDivisors B
⊢ (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • (algebraMap B L) y /
      (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • (algebraMap B L) z =
    x✝ • (algebraMap B L) y / x✝ • (algebraMap B L) z

Tactic:
subgroup_smul_def,

Goal state after:
case refine_2
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
E : Type u_6
inst✝¹¹ : Field E
inst✝¹⁰ : Algebra E L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(inertia G P)) E L
x✝ : ↥(inertia Gal(L/K) P)
y z : B
left✝ : z ∈ nonZeroDivisors B
⊢ ↑((P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝) • (algebraMap B L) y /
      ↑((P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝) • (algebraMap B L) z =
    ↑x✝ • (algebraMap B L) y / ↑x✝ • (algebraMap B L) z
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h.inr
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
⊢ ∃ n, a = a₁ ^ n

Tactic:
exact ⟨n + 1, by rw [pow_succ', ← hn, mul_comm a, ← mul_assoc, mul_inv_cancel, one_mul]⟩

Goal state after:
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
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ { q // (Polynomial.aeval z') F = q * z1 ^ 2 }

Tactic:
have hdzne : F.derivative.aeval z ≠ 0 :=
    mt norm_eq_zero.2 (by rw [hz.1]; apply deriv_norm_ne_zero; assumption)
  have hdzne' : (↑(F.derivative.aeval z) : ℚ_[p]) ≠ 0 := fun h => hdzne (Subtype.ext_iff.2 h)
  obtain ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion z (-z1)
  have : ‖(↑(F.derivative.aeval z) * (↑(F.aeval z) / ↑(F.derivative.aeval z)) : ℚ_[p])‖ ≤ 1 := by
    simpa using mul_le_one₀ (PadicInt.norm_le_one _) (norm_nonneg _) h1
  have : F.derivative.aeval z * -z1 = -F.aeval z := by
    calc
      F.derivative.aeval z * -z1 =
          F.derivative.aeval z * -⟨↑(F.aeval z) / ↑(F.derivative.aeval z), h1⟩ := by rw [hzeq]
      _ = -(F.derivative.aeval z * ⟨↑(F.aeval z) / ↑(F.derivative.aeval z), h1⟩) := mul_neg _ _
      _ = -⟨F.derivative.aeval z * (F.aeval z / (F.derivative.aeval z : ℤ_[p]) : ℚ_[p]), this⟩ :=
        (Subtype.ext <| by simp only [PadicInt.coe_neg, PadicInt.coe_mul])
      _ = -F.aeval z := by simp only [mul_div_cancel₀ _ hdzne', Subtype.coe_eta]
  exact ⟨q, by simpa [sub_eq_add_neg, neg_mul_eq_mul_neg, this, hz'] using hq⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁

Tactic:
· rw [x_neg, lt_neg] at Hx
    have := (x_zpow_pos (zero_lt_one.trans ha₁.1) n₂).trans Hx
    norm_num at this

Goal state after:
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
⊢ Tendsto (fun n ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)

Tactic:
rw [← mul_zero ‖F.derivative.aeval a‖, sq]

Goal state after:
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
⊢ Tendsto
    (fun n ↦
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ *
        T_gen p F a ^ 2 ^ n)
    atTop (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case hf
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
⊢ p ∈ d.primeFactors → 0 < s.nu p

Tactic:
hp

Goal state after:
case hf
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hp : p ∈ d.primeFactors
⊢ 0 < s.nu p
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0) =
    ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d

Tactic:
sum_comm

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0) =
    ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ (∑ d ∈ n.divisors, weights d) ^ 2 ≤
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
sum_comm

Goal state after:
case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ (∑ d ∈ n.divisors, weights d) ^ 2 ≤
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg.a
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ ∑ i ∈ n.divisors, weights i * weights d1 =
    ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
sum_comm

Goal state after:
case neg.a
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
⊢ ∑ i ∈ n.divisors, weights i * weights d1 =
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, if x = d1.lcm y then weights d1 * weights y else 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case pos
s : BoundingSieve
d : ℕ
h : d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

pp: case neg
s : BoundingSieve
d : ℕ
h : ¬d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

Tactic:
· simp [h]

Goal state after:
case neg
s : BoundingSieve
d : ℕ
h : ¬d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b : (Submodule.mkQ (map f p)) x ∈ Submodule.span R (Set.range (⇑(↑R (Submodule.mkQ (map f p))) ∘ b'))
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)

Tactic:
Set.range_comp,

Goal state after:
case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b : (Submodule.mkQ (map f p)) x ∈ Submodule.span R (⇑(↑R (Submodule.mkQ (map f p))) '' Set.range b')
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map f p)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1, -1)

Tactic:
obtain ⟨x, hx⟩ := hm

Goal state after:
m n : ℕ
hc : m.Coprime n
hn : IsSquare (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (-1, -1)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3

Tactic:
rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑(p * q) = ↑3
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
⊢ p ≠ 0 → ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p

Tactic:
hp

Goal state after:
case right
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
⊢ ‖P (f p) s‖ ≤ (c₁ * (c₂ * c' * c₃)) ^ p