mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n i j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hi : i.Coprime n
hj : j.Coprime n
this : ∀ {j : ℕ}, j.Coprime n → Associated (ζ - 1) (ζ ^ j - 1)
⊢ Associated (ζ ^ j - 1) (ζ ^ i - 1)

Tactic:
grind [Associated.trans, Associated.symm]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ ↑(nthRootsFinset p 1)
η₂ : A
⊢ η₂ ∈ ↑(nthRootsFinset p 1) → η₁ ≠ η₂ → (fun η₁ η₂ ↦ Associated (ζ - 1) (η₁ - η₂)) η₁ η₂

Tactic:
hη₂

Goal state after:
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ ↑(nthRootsFinset p 1)
η₂ : A
hη₂ : η₂ ∈ ↑(nthRootsFinset p 1)
⊢ η₁ ≠ η₂ → (fun η₁ η₂ ↦ Associated (ζ - 1) (η₁ - η₂)) η₁ η₂
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
by
  have h := prod_normalizedFactors (cyclotomic_ne_zero n K)
  have : ∀ P ∈ normalizedFactors (cyclotomic n K),
      P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f)) := fun P hP ↦
    natDegree_of_mem_normalizedFactors_cyclotomic hK hn hP
  have H := natDegree_eq_of_degree_eq <| degree_eq_degree_of_associated h
  rw [natDegree_cyclotomic, natDegree_multiset_prod _ (zero_notMem_normalizedFactors _),
    map_congr rfl this] at H
  simp only [map_const', sum_replicate, smul_eq_mul] at H
  rw [← H, mul_div_left _ (orderOf_pos _), toFinset_card_of_nodup]
  refine nodup_iff_count_le_one.mpr (fun P ↦ ?_)
  by_contra! H
  have : NeZero (n : K) := by
    refine ⟨fun H ↦ ?_⟩
    have := charP_of_card_eq_prime_pow hK
    exact hp.out.coprime_iff_not_dvd.mp ((coprime_pow_left_iff
      (pos_of_ne_zero <| f_ne_zero hK) _ _).mp (hn.pow_left f))
        ((CharP.cast_eq_zero_iff K p _).mp H)
  have hP : P ∈ normalizedFactors (cyclotomic n K) := count_pos.mp (by lia)
  refine (prime_of_normalized_factor _ hP).not_isUnit (squarefree_cyclotomic n K P ?_)
  have : {P, P} ≤ normalizedFactors (cyclotomic n K) := by
    refine le_iff_count.mpr (fun Q ↦ ?_)
    by_cases hQ : Q = P
    · simp only [hQ, insert_eq_cons, count_cons_self, nodup_singleton, mem_singleton,
        count_eq_one_of_mem, reduceAdd]
      lia
    · simp [hQ]
  have := prod_dvd_prod_of_le this
  simp only [insert_eq_cons, prod_cons, prod_singleton] at this
  exact this.trans h.dvd

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ p ^ 0 * (p - 1) = p - 1

Tactic:
pow_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ 1 * (p - 1) = p - 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
⊢ p ^ 0 * (p - 1) = p - 1

Tactic:
pow_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
⊢ 1 * (p - 1) = p - 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsBounded (↑expMapBasis '' closure (paramSet K))

Tactic:
exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p - 1

Tactic:
rw [← pow_one p] at hK
  rw [ramificationIdxIn_eq_of_prime_pow p 0, pow_zero, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 ^ nrComplexPlaces K)⁻¹ * 2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K *
      ENNReal.ofReal (regulator K) =
    2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
ENNReal.inv_mul_cancel_right (pow_ne_zero _ two_ne_zero)
    (pow_ne_top ENNReal.ofNat_ne_top)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) =
    2 ^ nrRealPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
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)
ha : a ≠ 0
hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a a_1 l.1 * (newBasis K) l.2)) b) = 0 (a_1, b)
⊢ a = 0

Tactic:
rw [← Matrix.ext_iff]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a a_1 l.1 * (newBasis K) l.2)) b) = 0 (a_1, b)
⊢ ∀ (i : α) (j : β), a i j = 0 i j
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
⊢ ∑ x, y ^ l.zipIdx[↑x].2 = ∑ i, y ^ ↑i

Tactic:
let e : Fin l.zipIdx.length ≃ Fin l.length := finCongr List.length_zipIdx

Goal state after:
T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
⊢ ∑ x, y ^ l.zipIdx[↑x].2 = ∑ i, y ^ ↑i
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ (∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩
  ext1 z
  rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ TotallyBounded Set.univ

Tactic:
refine Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, ball y ε
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)
⊢ 1 • r ^ 0 = 1

Tactic:
pow_zero,

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)
⊢ 1 • 1 = 1
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)
⊢ r ^ 0 + r ^ 1 = 1 + r

Tactic:
pow_zero,

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)
⊢ 1 + r ^ 1 = 1 + r
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
this : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)

Tactic:
rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom,
      ← Int.cast_natCast, this, eval₂_hom, Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]

Goal state after:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
this : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ eval (↑b) (cyclotomic k ℤ)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
hn : 0 < n
⊢ 0 < (a ^ n).y

Tactic:
lift n to ℕ using hn.le

Goal state after:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < ↑n
⊢ 0 < (a ^ ↑n).y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ Int.negSucc n).x

Tactic:
rw [zpow_negSucc]
    exact x_pow_pos hax (n + 1)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℤ
⊢ 0 < (a ^ n).x

Tactic:
by
  cases n with
  | ofNat n =>
    rw [Int.ofNat_eq_natCast, zpow_natCast]
    exact x_pow_pos hax n
  | negSucc n =>
    rw [zpow_negSucc]
    exact x_pow_pos hax (n + 1)

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
h : ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 < 1
⊢ T_gen p F a < 1

Tactic:
rw [T_def]

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
h : ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 < 1
⊢ ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 < 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
⊢ ↑q₂.num ^ 2 - ↑d * (↑q₂.den * ↑q₂.den) = 0

Tactic:
← sq

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
⊢ ↑q₂.num ^ 2 - ↑d * ↑q₂.den ^ 2 = 0
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
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ p • Submodule.span R (Set.range a)

Tactic:
{

Goal state after:
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ p • Submodule.span R (Set.range a)
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⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
⊢ { q // (Polynomial.aeval z') F = q * z1 ^ 2 }

Tactic:
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]

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
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⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this✝ :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
this : (Polynomial.aeval z) (Polynomial.derivative F) * -z1 = -(Polynomial.aeval z) F
⊢ { q // (Polynomial.aeval z') F = q * z1 ^ 2 }
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Module.finrank K D * Module.finrank D E = Module.finrank K E
⊢ Module.finrank D E = p.inertiaDegIn B

Tactic:
IsInertiaField.rank_right A K L P E hp,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Module.finrank K D * Module.finrank D E = (p.primesOver B).ncard * p.inertiaDegIn B
⊢ Module.finrank D E = p.inertiaDegIn B
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: 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
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : IsFractionRing B L
inst✝¹⁴ : MulSemiringAction Gal(L/K) B
inst✝¹³ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
inst✝⁹ : CommRing 𝓞D
inst✝⁸ : Algebra 𝓞D D
inst✝⁷ : IsFractionRing 𝓞D D
inst✝⁶ : Algebra 𝓞D B
inst✝⁵ : Algebra 𝓞D L
inst✝⁴ : IsScalarTower 𝓞D D L
inst✝³ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
hP : P.IsPrime
inst✝² : Finite ↥(stabilizer Gal(L/K) P)
inst✝¹ : IsIntegrallyClosed 𝓞D
inst✝ : Algebra.IsIntegral 𝓞D B
this : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
⊢ ∀ x ∈ 𝓟D.primesOver B, x = P

Tactic:
rintro Q ⟨_, _⟩

Goal state after:
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
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : IsFractionRing B L
inst✝¹⁴ : MulSemiringAction Gal(L/K) B
inst✝¹³ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
inst✝⁹ : CommRing 𝓞D
inst✝⁸ : Algebra 𝓞D D
inst✝⁷ : IsFractionRing 𝓞D D
inst✝⁶ : Algebra 𝓞D B
inst✝⁵ : Algebra 𝓞D L
inst✝⁴ : IsScalarTower 𝓞D D L
inst✝³ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
hP : P.IsPrime
inst✝² : Finite ↥(stabilizer Gal(L/K) P)
inst✝¹ : IsIntegrallyClosed 𝓞D
inst✝ : Algebra.IsIntegral 𝓞D B
this : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
Q : Ideal B
left✝ : Q.IsPrime
right✝ : Q.LiesOver 𝓟D
⊢ Q = P
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
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
z' : ℤ_[p] := z - z1
⊢ ‖z1‖ = ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
simp [z1, hz.1]

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
n : ℕ
⊢ ‖newton_seq (n + 1) - newton_seq n‖ =
    ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval (newton_seq n)) (Polynomial.derivative F)‖

Tactic:
by
  rw [newton_seq_gen, newton_seq_gen, newton_seq_aux, ih_n]
  simp [sub_eq_add_neg, add_comm]

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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ T_gen p F a > 0

Tactic:
rw [T_def]

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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 > 0
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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ <
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

pp: case hnsol
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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ (Polynomial.aeval a) F ≠ 0

Tactic:
← 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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

case hnsol
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
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ (Polynomial.aeval a) F ≠ 0