mathlib-initiative/mathlib-tactics huggingface dataset:
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 ^ 2 = 0

Tactic:
]

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.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 ^ 2 ∣ q₂.num ^ 2 - d * ↑q₂.den ^ 2

Tactic:
]

Goal state after:
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)
⊢ ↑(q₂.num * ↑q₁.den) = ↑(q₁.num * ↑q₂.den)

Tactic:
]

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
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
⊢ ↑(q₂.num * ↑q₁.den) = ↑(q₁.num * ↑q₂.den)
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)
⊢ ↑q₂.num * ↑q₂.den = ↑q₂.num * ↑q₂.den

Tactic:
]

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
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) = ⊤
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

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) = ⊤
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
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) = ⊤
⊢ p • ⊤ = p • ⊤

Tactic:
]

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
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) = ⊤
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False

Tactic:
]

Goal state after:
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ x ^ 2 - d * y ^ 2 = 1

Tactic:
]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ x ^ 2 - d * y ^ 2 = 1
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 ∈ ⊤

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 ∈ ⊤
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2

Tactic:
]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2

Tactic:
exact mul_pos h₀ (sq_pos_of_ne_zero hy)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ b.x ^ 2 - 1 = b.x ^ 2 - 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ 1 < ↑x₁

Tactic:
]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ 1 < ↑x₁
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
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∑ i, (fun i ↦ a'' i) i • a i = ∑ i, a'' i • a i

pp: case h
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
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∀ (i : Fin n), 0 • a i = 0

Tactic:
]

Goal state after:
case h
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
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∀ (i : Fin n), 0 • a i = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ ↑x₁ ≤ b.x

Tactic:
]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ ↑x₁ ≤ b.x
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
⊢ (Polynomial.aeval z) (Polynomial.derivative F) *
      -⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩ =
    (Polynomial.aeval z) (Polynomial.derivative F) *
      -⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < ↑b.x.toNat
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ ↑b.x.toNat

Tactic:
]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < ↑b.x.toNat
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ ↑b.x.toNat
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ b.x ^ 2 - d * b.y ^ 2 = 1

Tactic:
]

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ b.x ^ 2 - d * b.y ^ 2 = 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + ((a ^ n).y * a.x - (a ^ n).y)

Tactic:
]

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + ((a ^ n).y * a.x - (a ^ n).y)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + (a ^ n).y * (a.x - 1)

Tactic:
]

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + (a ^ n).y * (a.x - 1)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x

Tactic:
]

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x
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
n : ℤ
hn : n < 0
m : ℤ := -n - 1
⊢ n = -m - 1

Tactic:
simp only [m, neg_sub, sub_neg_eq_add, add_tsub_cancel_left]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
hm,

Goal state after:
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ (a ^ (-m - 1)).y < (a ^ (-m - 1 + 1)).y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ (a ^ m).y < (a ^ (m + 1)).y

Tactic:
]

Goal state after:
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ (a ^ m).y < (a ^ (m + 1)).y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = a ^ 0 ↔ n = 0

Tactic:
]

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = a ^ 0 ↔ n = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False

Tactic:
]

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False
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
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = 1 + d * a₁.y ^ 2 - (1 + d * a.y ^ 2)

Tactic:
]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = 1 + d * a₁.y ^ 2 - (1 + d * a.y ^ 2)
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)
x : L
⊢ (P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • x = x✝ • x

Tactic:
obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x
    simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
      inertiaEquiv_symm_apply_smul]

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
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ≤ a.x

Tactic:
]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ≤ a.x
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case calc_2
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
i : Fin n
⊢ ∑ y, ∑ x, (B i y * A y x) • a x = ∑ x, ∑ x_1, (B i x * A x x_1) • a x_1

Tactic:
]

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
⊢ |a.x| * |a₁.y| ≤ |a.y| * |a₁.x|

Tactic:
← abs_mul,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a.x * a₁.y| ≤ |a.y| * |a₁.x|
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
⊢ |a.x * a₁.y| ≤ |a.y| * |a₁.x|

Tactic:
← abs_mul,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a.x * a₁.y| ≤ |a.y * a₁.x|
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
⊢ 0 ≤ a.y ^ 2 * (1 + d * a₁.y ^ 2) - (1 + d * a.y ^ 2) * a₁.y ^ 2

Tactic:
]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ a.y ^ 2 * (1 + d * a₁.y ^ 2) - (1 + d * a.y ^ 2) * a₁.y ^ 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
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Finite (A ⧸ p)
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = p.ramificationIdxIn B * p.inertiaDegIn B

Tactic:
]

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
⊢ a₁.y ≤ a.y

Tactic:
]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y
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
⊢ a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y)

Tactic:
by ring

Goal state after: