mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
<;>

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 - 1
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 4 ∣ S.Y ^ 3 + 1
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
<;>

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 - 1
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 4 ∣ S.Z ^ 3 + 1
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
<;>

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 - 1
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HY : λ ^ 2 ∣ S.Y ^ 3 + 1
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
<;>

Goal state after:
case inl.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inl.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
Y : 𝓞 K
hY : S.Y ^ 3 - 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 - 1
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
HZ : λ ^ 2 ∣ S.Z ^ 3 + 1
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, v (x i)

pp: case inr.e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, ↑v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, ↑v (x i)

Tactic:
<;>

Goal state after:
case inr.e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, v (x i)

case inr.e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
⊢ (fun v ↦ ⨆ i, ↑v (Sum.elim x 0 i)) = fun v ↦ ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
he : vecCons 0 x ∘ ⇑e = Sum.elim x 0
⊢ mulHeight (Sum.elim x 0) = mulHeight x

Tactic:
mulHeight_sumElim_zero_eq

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
he : vecCons 0 x ∘ ⇑e = Sum.elim x 0
⊢ mulHeight x = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hf
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-s)) volume (↑n) (↑n + 1)

pp: case hg
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-(s + 1))) volume (↑n) (↑n + 1)

Tactic:
<;>

Goal state after:
case hf
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-s)) volume (↑n) (↑n + 1)

case hg
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-(s + 1))) volume (↑n) (↑n + 1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl.zero
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
⊢ mulHeight (0 ^ 0) = mulHeight 0 ^ 0

pp: case inl.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
n✝ : ℕ
⊢ mulHeight (0 ^ (n✝ + 1)) = mulHeight 0 ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case inl.zero
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
⊢ mulHeight (0 ^ 0) = mulHeight 0 ^ 0

case inl.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
n✝ : ℕ
⊢ mulHeight (0 ^ (n✝ + 1)) = mulHeight 0 ^ (n✝ + 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case b0.refine_1
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

pp: case b0.refine_2
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

Tactic:
<;>

Goal state after:
case b0.refine_1
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

case b0.refine_2
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case b0
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod

Tactic:
refine mul_nonneg (mul_nonneg (by simp) ?_) ?_ <;>
      exact prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _

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

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun i ↦ i) ⟨0, ⋯⟩) = ![1, x] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun i ↦ i) ⟨1, ⋯⟩) = ![1, x] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun i ↦ i) ⟨0, ⋯⟩) = ![1, x] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun i ↦ i) ⟨1, ⋯⟩) = ![1, x] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.u₄ = 1
⊢ S.u₄ ^ 2 = 1

pp: case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.u₄ = -1
⊢ S.u₄ ^ 2 = 1

Tactic:
<;>

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.u₄ = 1
⊢ S.u₄ ^ 2 = 1

case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.u₄ = -1
⊢ S.u₄ ^ 2 = 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
⊢ term n s = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
by
  have hv : ∀ x ∈ uIcc (n : ℝ) (n + 1), 0 < x := by
    intro x hx
    rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
    exact (Nat.cast_pos.mpr hn).trans_le hx.1
  calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
      · rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
x : Fin 3 → K
⊢ (logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x ≤ max C₁ (-C₂)

pp: case refine_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
x : Fin 3 → K
⊢ (2 * logHeight x - logHeight fun i ↦ (eval x) (W.addSubMap i)) ≤ max C₁ (-C₂)

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
x : Fin 3 → K
⊢ (logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x ≤ max C₁ (-C₂)

case refine_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
x : Fin 3 → K
⊢ (2 * logHeight x - logHeight fun i ↦ (eval x) (W.addSubMap i)) ≤ max C₁ (-C₂)