mathlib-initiative/mathlib-tactics huggingface dataset:
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)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) = -q * h
⊢ ‖q‖ * ‖h‖ ≤ 1 * ‖h‖

Tactic:
gcongr

Goal state after:
case hbc
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)‖
h : ℤ_[p] := ⋯
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) = -q * h
⊢ ‖q‖ ≤ 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]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
gcongr

Goal state after:
case hab
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
⊢ ‖(Polynomial.aeval z) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
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
hz1 : ‖z1‖ = ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
gcongr

Goal state after:
case hab
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
hz1 : ‖z1‖ = ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖(Polynomial.aeval z) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
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
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Tactic:
replace hm₀ : (m : ℚ) ≠ 0 := Int.cast_ne_zero.mpr hm₀

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
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
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this✝ : a.x * a₁.y ≤ a.y * a₁.x
this : 0 < d
⊢ d * a.y * (a.x * a₁.y) ≤ d * a.y * (a.y * a₁.x)

Tactic:
gcongr

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this✝ : 1 < a₁.x
this : a.x * a₁.y ≤ a.y * a₁.x
⊢ a.x * a₁.y * a₁.x ≤ a.y * a₁.x * a₁.x

Tactic:
gcongr

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]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
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‖ * ‖z1‖ ^ 2 ≤ 1 * ‖z1‖ ^ 2

Tactic:
gcongr

Goal state after:
case hbc
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]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
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‖ ≤ 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]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
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⟩
⊢ ‖(Polynomial.aeval z) F‖ ^ 2 / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 ≤
    (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

Tactic:
gcongr

Goal state after:
case hab
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]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
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⟩
⊢ ‖(Polynomial.aeval z) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
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 : ℕ
⊢ ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
gcongr

Goal state after:
case hab
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 : ℕ
⊢ ‖(Polynomial.aeval (newton_seq n)) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: case refine_4
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✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A 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
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ 𝓟D.inertiaDegIn B ≤ p.inertiaDegIn B

Tactic:
inertiaDegIn_eq_inertiaDeg p P Gal(L/K),

Goal state after:
case refine_4
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✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A 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
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ 𝓟D.inertiaDegIn B ≤ P.inertiaDeg A
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 • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ S ∙ f A.det
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i, a' i • a i = Submodule.Quotient.mk x'
| ∑ x, A.det • a' x • a x = 0

Tactic:
lhs; congr; next => skip
      intro x; rw [smul_comm A.det, d_smul, smul_zero]

Goal state after:
case f
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 • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : A.det • x' ∈ S ∙ f A.det
a' : Fin n → R
left✝ : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : ∑ i, a' i • a i = Submodule.Quotient.mk x'
x : Fin n
| 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
z : ℤ_[p]
hev : (Polynomial.aeval z) F = 0
hnlt : ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖z - soln‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
calc
      ‖z - soln‖ = ‖z - a + (a - soln)‖ := by rw [sub_add_sub_cancel]
      _ ≤ max ‖z - a‖ ‖a - soln‖ := PadicInt.nonarchimedean _ _
      _ < ‖F.derivative.aeval a‖ :=
        max_lt hnlt ((norm_sub_rev soln a ▸ (soln_dist_to_a_lt_deriv hnorm)) hnsol)

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ 0 < ⌈↑k * s⌉ - 1

Tactic:
sub_pos,

Goal state after:
case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ 1 < ⌈↑k * s⌉
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq' s✝ k = x}
k : ℤ
hj : 0 < ⌈↑k * s✝⌉ - 1
hk : beattySeq' s✝ k = j
⊢ k > 0

Tactic:
sub_pos,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq' s✝ k = x}
k : ℤ
hj : 1 < ⌈↑k * s✝⌉
hk : beattySeq' s✝ k = j
⊢ k > 0
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
hr : Irrational r
x✝ k : ℤ
⊢ k > 0 ∧ ⌈↑k * r⌉ - 1 = x✝ ↔ k > 0 ∧ ⌊↑k * r⌋ = x✝

Tactic:
rw [and_congr_right_iff]

Goal state after:
r : ℝ
hr : Irrational r
x✝ k : ℤ
⊢ k > 0 → (⌈↑k * r⌉ - 1 = x✝ ↔ ⌊↑k * r⌋ = x✝)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg.a.a.h
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ d1.lcm d2 ∣ n ∧ n ≠ 0

Tactic:
Nat.lcm_dvd_iff

Goal state after:
case neg.a.a.h
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
d1 : ℕ
hd1 : d1 ∈ n.divisors
d2 : ℕ
hd2 : d2 ∈ n.divisors
⊢ (d1 ∣ n ∧ d2 ∣ n) ∧ n ≠ 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd_pos : 0 < d
⊢ d ∣ s.prodPrimes → ∑ a ∈ d.divisors, (selbergTerms a)⁻¹ = (s.nu d)⁻¹

Tactic:
revert d

Goal state after:
s : BoundingSieve
⊢ ∀ {d : ℕ}, 0 < d → d ∣ s.prodPrimes → ∑ a ∈ d.divisors, (selbergTerms a)⁻¹ = (s.nu d)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (selbergTerms d * ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then (selbergTerms l)⁻¹ else 0) = selbergTerms d * (s.nu d)⁻¹

Tactic:
← nu_inv_eq_sum_divisors_inv_selbergTerms hd

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ selbergTerms d * (s.nu d)⁻¹ = selbergTerms d * (s.nu d)⁻¹
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: a b x y u v : ℕ
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ ∃ r s, a * b = r ^ 2 + s ^ 2

Tactic:
zify at ha hb ⊢
  obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb
  refine ⟨r.natAbs, s.natAbs, ?_⟩
  simpa only [Int.natCast_natAbs, sq_abs]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℂ[X]
s : ℂ
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)

Tactic:
rw [integral_exp_mul_eval, mul_add, mul_neg, exp_neg, mul_inv_cancel_left₀ (exp_ne_zero s),
    neg_add_eq_sub, P]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ Real.exp s.re * (‖∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)‖ * ‖s‖) ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
gcongr

Goal state after:
case hbc
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Submodule.Quotient.mk x) =
    Submodule.Quotient.mk ⟨(Quotient.mk (P ^ e)) (a * x), ⋯⟩

Tactic:
by
  apply Quotient.map'_mk''

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case hbc.convert_11
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ Real.exp (-(x • s)).re * ‖eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p

Tactic:
gcongr

Goal state after:
case a
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ (-(x • s)).re ≤ ‖s‖

case h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p
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 : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖) ≤ c₁ ^ p * (c₂ ^ p * c' ^ p * c₃ ^ p)

Tactic:
gcongr

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

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

case h₂
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ ‖s‖ ≤ c₃ ^ p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
⊢ f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)

Tactic:
← natAbs_iff,

Goal state after:
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
⊢ (f b).natAbs ^ 2 + (f a).natAbs ^ 2 + (f d).natAbs ^ 2 + (-f c).natAbs ^ 2 = m * r
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
⊢ (f b).natAbs ^ 2 + (f a).natAbs ^ 2 + (f d).natAbs ^ 2 + (-f c).natAbs ^ 2 = m * r

Tactic:
natAbs_neg,

Goal state after:
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
⊢ (f b).natAbs ^ 2 + (f a).natAbs ^ 2 + (f d).natAbs ^ 2 + (f c).natAbs ^ 2 = m * r