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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.algEquiv h') (h.map z) = ((↑(h.algEquiv h')).comp h.map) z

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.algEquiv h') (h.map z) = ((↑(h.algEquiv h')).comp h.map) z
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], ↑(Fintype.card F) - 2 = -1 + z * (μ - 1) ^ 2

Tactic:
]

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], ↑(Fintype.card F) - 2 = -1 + z * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
ha : mulHeight ![↑a, ↑n] ≤ B
⊢ IsIntegral ℤ ↑a ∧ mulHeight ![↑a, ↑n] ≤ B

Tactic:
]

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
ha : mulHeight ![↑a, ↑n] ≤ B
⊢ IsIntegral ℤ ↑a ∧ mulHeight ![↑a, ↑n] ≤ B
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ z₁ * (μ - 1) ^ 2 * ↑q + ↑1 - 2 = -1 + ↑q * z₁ * (μ - 1) ^ 2

Tactic:
]

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ z₁ * (μ - 1) ^ 2 * ↑q + ↑1 - 2 = -1 + ↑q * z₁ * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
x✝¹ : a ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
b : 𝓞 K
x✝ : b ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
h : a = b
⊢ a = b

Tactic:
]

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
x✝¹ : a ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
b : 𝓞 K
x✝ : b ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
h : a = b
⊢ a = b
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : f ∣ h.repr z - w
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : f ∣ h.repr z - w
⊢ eval₂ i x (h.repr z) = eval₂ i x w
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
a : 𝓞 K
ha : ↑n * x = ↑a
⊢ mulHeight₁ x ≤ B

Tactic:
]

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
x : K
x✝ : x ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}
hx₁ : IsIntegral ℤ (↑n * x)
hx₂ : mulHeight₁ x ≤ B
a : 𝓞 K
ha : ↑n * x = ↑a
⊢ mulHeight₁ x ≤ B
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ¬ψ = 1
⊢ -1 = -1

Tactic:
]

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

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
refine ⟨0, Subalgebra.zero_mem _, ?_⟩
    rw [hχ₀, jacobiSum_one_nontrivial hψ₀, zero_mul, add_zero]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
n : ℕ
hn₀ : n ≠ 0
hn₁ : ↑n ≤ mulHeight₁ x
hn : IsIntegral ℤ (↑n * x)
h : mulHeight₁ x ≤ B
⊢ IsIntegral ℤ (↑n * x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
n : ℕ
hn₀ : n ≠ 0
hn₁ : ↑n ≤ mulHeight₁ x
hn : IsIntegral ℤ (↑n * x)
h : mulHeight₁ x ≤ B
⊢ IsIntegral ℤ (↑n * x)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
H : {x | mulHeight₁ x ≤ B} = ⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}
⊢ (⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}).Finite

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
H : {x | mulHeight₁ x ≤ B} = ⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}
⊢ (⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}).Finite
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ψ = 1
⊢ -1 = -1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap : ∀ (a : R), g ((algebraMap R S) a) = i a
hroot : g h.root = x
a : S
⊢ g (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i)) =
    (h.lift i x hx) (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i))

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap : ∀ (a : R), g ((algebraMap R S) a) = i a
hroot : g h.root = x
a : S
⊢ g (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i)) =
    (h.lift i x hx) (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ], 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) = -1 + z * (μ - 1) ^ 2

Tactic:
]

Goal state after:
case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ], 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) = -1 + z * (μ - 1) ^ 2
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : CommRing T
x : T
inst✝ : Algebra R T
hx' : (aeval x) f = 0
z : R[X]
⊢ eval₂ (algebraMap R T) x z = eval₂ (algebraMap R T) x z

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : CommRing T
x : T
inst✝ : Algebra R T
hx' : (aeval x) f = 0
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hf : 1 ≤ v ↑(x i) * v ↑(f i)
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hf : 1 ≤ v ↑(x i) * v ↑(f i)
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ f * (g /ₘ f)

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ f * (g /ₘ f)
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ h.map g = h.map g

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ Finset.univ.gcd x ≠ 1

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ Finset.univ.gcd x ≠ 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ 0 ≠ 1

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ 0 ≠ 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
⊢ log ↑(⨆ i, |x i|) = log ↑(⨆ i, |x i|)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
⊢ c • (h.repr x %ₘ f) = c • (h.repr x %ₘ f)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: q : ℚ
hq₀ : ↑q.den ≠ 0
⊢ mulHeight (↑q.den • ![q, 1]) = mulHeight ![↑q.num, ↑q.den]

Tactic:
]

Goal state after:
q : ℚ
hq₀ : ↑q.den ≠ 0
⊢ mulHeight (↑q.den • ![q, 1]) = mulHeight ![↑q.num, ↑q.den]
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: q : ℚ
⊢ mulHeight ![↑q.num, ↑↑q.den] = ↑(max q.num.natAbs q.den)

Tactic:
]

Goal state after:
q : ℚ
⊢ mulHeight ![↑q.num, ↑↑q.den] = ↑(max q.num.natAbs q.den)
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ ↑n < f.degree

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ ↑n < f.degree
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ C * mulHeight ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ≤ mulHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝]

Tactic:
]

Goal state after:
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ C * mulHeight ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ≤ mulHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝]
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ x = x

pp: case hf
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ Function.Injective Fin.val

pp: case hl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ ↑(h.modByMonicHom x).toFinsupp.coeff.support ⊆ Set.range Fin.val

Tactic:
]

Goal state after:
case hf
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ Function.Injective Fin.val

case hl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ ↑(h.modByMonicHom x).toFinsupp.coeff.support ⊆ Set.range Fin.val
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑(max q.num.natAbs q.den) = ⨆ i, |![q.num, ↑q.den] i|

Tactic:
]

Goal state after:
case e'_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑(max q.num.natAbs q.den) = ⨆ i, |![q.num, ↑q.den] i|
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff ↑i = g i

pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff ↑i = g i

R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ g i = g i

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ ∀ (m : ℕ), f.natDegree ≤ m → { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ ∀ (m : ℕ), f.natDegree ≤ m → { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff m = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff m = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ 0 = 0

pp: case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ m ∉ Set.range Fin.val

Tactic:
]

Goal state after:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ m ∉ Set.range Fin.val
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ ∀ (x : Fin f.natDegree), ¬↑x = m

Tactic:
]

Goal state after:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ ∀ (x : Fin f.natDegree), ¬↑x = m
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: q : ℚ
⊢ log ↑(max q.num.natAbs q.den) = log ↑(max q.num.natAbs q.den)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.root = h.root

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)} =
    span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
⊢ (if hi : i < f.natDegree then (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ else 0) = Pi.single n 1 i

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
⊢ (if hi : i < f.natDegree then (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ else 0) = Pi.single n 1 i
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ = (h.basis.repr (h.root ^ n)) ⟨i, hi⟩

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))
      (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))
      (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))