awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
h : ∀ (j : Fin n ⊕ Fin 1), (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) j = Sum.elim x 0 j
⊢ Eq (α := Fin n ⊕ Fin 1 → K) (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) (Sum.elim x 0)

Tactic:
ext j : 1
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
j : Fin n ⊕ Fin 1
val : Fin n
⊢ Function.comp (α := Fin n ⊕ Fin 1) (vecCons 0 x) (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ) (Sum.inl val) =
    Sum.elim (β := Fin 1) x 0 (Sum.inl val)

Tactic:
simp [e]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
j : Fin n ⊕ Fin 1
i : ℕ
h : i < 1
⊢ i = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
j : Fin n ⊕ Fin 1
i : ℕ
h : i < 1
⊢ Function.comp (α := Fin n ⊕ Fin 1) (vecCons 0 x) (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ) (Sum.inr (⟨i, h⟩ : Fin 1)) =
    Sum.elim x 0 (Sum.inr (⟨i, h⟩ : Fin 1))

Tactic:
simp [show i = 0 by lia, e, show Fin.castAdd n 0 = 0 from Fin.castAdd_mk _ _ zero_lt_one]

Premises used: Fin.castAdd_mk, zero_lt_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
j : Fin n ⊕ Fin 1
⊢ (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) j = Sum.elim x 0 j

Tactic:
match j with
    | .inl _ => simp [e]
    | .inr ⟨i, h⟩ =>
      simp [show i = 0 by lia, e, show Fin.castAdd n 0 = 0 from Fin.castAdd_mk _ _ zero_lt_one]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
⊢ Eq (α := Fin n ⊕ Fin 1 → K) (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) (Sum.elim x 0)

Tactic:
have he : Matrix.vecCons 0 x ∘ ⇑e = Sum.elim x 0 := by
    ext j : 1
    match j with
    | .inl _ => simp [e]
    | .inr ⟨i, h⟩ =>
      simp [show i = 0 by lia, e, show Fin.castAdd n 0 = 0 from Fin.castAdd_mk _ _ zero_lt_one]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := Equiv.trans (Equiv.sumComm (Fin n) (Fin 1)) (Equiv.trans finSumFinEquiv (finCongr ⋯))
he : Eq (α := Fin n ⊕ Fin 1 → K) (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) (Sum.elim x 0)
rw : mulHeight (ι := Fin n ⊕ Fin 1) (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) = mulHeight x
rw₁ : mulHeight (ι := Fin n ⊕ Fin 1) (Sum.elim x 0) = mulHeight x
rw₂ rw₃ : mulHeight x = mulHeight x
⊢ mulHeight (vecCons 0 x) = mulHeight x

Tactic:
rw [← mulHeight_comp_equiv e, he, mulHeight_sumElim_zero_eq]

Premises used: Height.mulHeight_comp_equiv, Height.mulHeight_sumElim_zero_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
⊢ logHeight (vecCons 0 x) = logHeight x

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
rw :
  mulHeight (ι := Fin n.succ.succ)
      (vecCons a (vecCons 0 x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ)) =
    mulHeight (vecCons a x)
⊢ mulHeight (vecCons a (vecCons 0 x)) = mulHeight (vecCons a x)

Tactic:
rw [← mulHeight_comp_equiv (Equiv.swap 0 1)]

Premises used: Equiv.swap, Height.mulHeight_comp_equiv, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ mulHeight (ι := Fin n.succ.succ)
      (vecCons a (vecCons 0 x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ)) =
    mulHeight (vecCons a x)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ logHeight (vecCons a (vecCons 0 x)) = logHeight (vecCons a x)

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
rw :
  mulHeight (ι := Fin (n + 2 + 1))
      (vecCons a (vecCons b (vecCons 0 x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ))) =
    mulHeight (vecCons a (vecCons b x))
⊢ mulHeight (vecCons a (vecCons b (vecCons 0 x))) = mulHeight (vecCons a (vecCons b x))

Tactic:
rw [← mulHeight_comp_equiv (Equiv.swap (Fin.succ 0) (Fin.succ 1)), ← cons_swap]

Premises used: Fin.succ, Matrix.cons_swap, Equiv.swap, Height.mulHeight_comp_equiv, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ mulHeight (ι := Fin (n + 2 + 1))
      (vecCons a (vecCons b (vecCons 0 x) ∘ (⇑(Equiv.swap 0 1) : (a : Fin n.succ.succ) → Fin n.succ.succ))) =
    mulHeight (vecCons a (vecCons b x))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ logHeight (vecCons a (vecCons b (vecCons 0 x))) = logHeight (vecCons a (vecCons b x))

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
⊢ logHeight (c • x) = logHeight x

Tactic:
simp only [logHeight_eq_log_mulHeight, mulHeight_smul_eq_mulHeight x hc]

Premises used: Height.mulHeight_smul_eq_mulHeight, Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x_1 : K
v : AbsoluteValue K ℝ
x : K
i : Fin 2
0 :
  Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) : ℝ)
    (![(v : (a : K) → ℝ) x, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
1 :
  Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) : ℝ)
    (![(v : (a : K) → ℝ) x, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] i) : ℝ) (![(v : (a : K) → ℝ) x, 1] i : ℝ)

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x_1 : K
v : AbsoluteValue K ℝ
x : K
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))) : ℝ)
    (![(v : (a : K) → ℝ) x, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x_1 : K
v : AbsoluteValue K ℝ
x : K
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))) : ℝ)
    (![(v : (a : K) → ℝ) x, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x_1 : K
v : AbsoluteValue K ℝ
x : K
⊢ ∀ (i : Fin 2), Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] i) : ℝ) (![(v : (a : K) → ℝ) x, 1] i : ℝ)

Tactic:
have (i : Fin 2) : v (![x, 1] i) = ![v x, 1] i := by fin_cases i <;> simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x_1 : K
v : AbsoluteValue K ℝ
x : K
this : ∀ (i : Fin 2), Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] i) : ℝ) (![(v : (a : K) → ℝ) x, 1] i : ℝ)
⊢ Eq (α := ℝ) (max ((v : (a : K) → ℝ) x) 1 : ℝ) (⨆ (i : Fin (Nat.succ 0).succ), (v : (a : K) → ℝ) (![x, 1] i) : ℝ)

Tactic:
simpa [this] using max_eq_iSup (v x) 1

Premises used: _private.0.Height.max_eq_iSup, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ ∀ (v : AbsoluteValue K ℝ) (x : K),
    Eq (α := ℝ) (max ((v : (a : K) → ℝ) x) 1 : ℝ) (⨆ (i : Fin (Nat.succ 0).succ), (v : (a : K) → ℝ) (![x, 1] i) : ℝ)

Tactic:
have H (v : AbsoluteValue K ℝ) (x : K) : v x ⊔ 1 = ⨆ i, v (![x, 1] i) := by
    have (i : Fin 2) : v (![x, 1] i) = ![v x, 1] i := by fin_cases i <;> simp
    simpa [this] using max_eq_iSup (v x) 1
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  ∀ (v : AbsoluteValue K ℝ) (x : K),
    Eq (α := ℝ) (max ((v : (a : K) → ℝ) x) 1 : ℝ) (⨆ (i : Fin (Nat.succ 0).succ), (v : (a : K) → ℝ) (![x, 1] i) : ℝ)
⊢ ![x, 1] ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  ∀ (v : AbsoluteValue K ℝ) (x : K),
    Eq (α := ℝ) (max ((v : (a : K) → ℝ) x) 1 : ℝ) (⨆ (i : Fin (Nat.succ 0).succ), (v : (a : K) → ℝ) (![x, 1] i) : ℝ)
⊢ ![x, 1] ≠ 0

Tactic:
have hx : ![x, 1] ≠ 0 := by simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  ∀ (v : AbsoluteValue K ℝ) (x : K),
    Eq (α := ℝ) (max ((v : (a : K) → ℝ) x) 1 : ℝ) (⨆ (i : Fin (Nat.succ 0).succ), (v : (a : K) → ℝ) (![x, 1] i) : ℝ)
hx : ![x, 1] ≠ 0
⊢ mulHeight₁ x = mulHeight ![x, 1]

Tactic:
simp only [mulHeight₁_eq, mulHeight_eq hx, H]

Premises used: Height.mulHeight₁_eq, Height.mulHeight_eq
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ logHeight₁ x = logHeight ![x, 1]

Tactic:
simp only [logHeight₁_eq_log_mulHeight₁, logHeight_eq_log_mulHeight, mulHeight₁_eq_mulHeight x]

Premises used: Height.logHeight_eq_log_mulHeight, Height.mulHeight₁_eq_mulHeight, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
inl : mulHeight₁ (x / 0) = mulHeight ![x, 0]
inr : ∀ (hy : y ≠ 0), mulHeight₁ (x / y) = mulHeight ![x, y]
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ (x / 0) = mulHeight ![x, 0]

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
hy : y ≠ 0
inr : mulHeight (y • ![x / y, 1]) = mulHeight ![x, y]
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]

Tactic:
rw [mulHeight₁_eq_mulHeight, ← mulHeight_smul_eq_mulHeight _ hy]

Premises used: Height.mulHeight_smul_eq_mulHeight, Height.mulHeight₁_eq_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
hy : y ≠ 0
⊢ mulHeight (y • ![x / y, 1]) = mulHeight ![x, y]

Tactic:
simp [mul_div_cancel₀ x hy]

Premises used: mul_div_cancel₀
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x y : K
rw : log (mulHeight₁ (x / y)) = logHeight ![x, y]
rw₁ : log (mulHeight₁ (x / y)) = log (mulHeight ![x, y])
rw₂ rw₃ : log (mulHeight ![x, y]) = log (mulHeight ![x, y])
⊢ logHeight₁ (x / y) = logHeight ![x, y]

Tactic:
rw [logHeight₁_eq_log_mulHeight₁, logHeight_eq_log_mulHeight, mulHeight₁_div_eq_mulHeight x y]

Premises used: Height.logHeight_eq_log_mulHeight, Height.mulHeight₁_div_eq_mulHeight, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
inl : mulHeight (HPow.hPow (α := ι → K) 0 n) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ n
inr : ∀ (hx : x ≠ 0), mulHeight (x ^ n) = mulHeight x ^ n
⊢ mulHeight (x ^ n) = mulHeight x ^ n

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
n : ℕ
inl : mulHeight (HPow.hPow (α := ι → K) (β := ℕ) 0 0) = HPow.hPow (β := ℕ) (mulHeight.{u_1, u_2} (K := K) (ι := ι) 0) 0
inl₁ : ∀ (n : ℕ), mulHeight (HPow.hPow (α := ι → K) 0 (n + 1)) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ (n + 1)
⊢ mulHeight (HPow.hPow (α := ι → K) 0 n) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ n

Tactic:
cases n
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
⊢ mulHeight (HPow.hPow (α := ι → K) (β := ℕ) 0 0) = HPow.hPow (β := ℕ) (mulHeight.{u_1, u_2} (K := K) (ι := ι) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
n : ℕ
⊢ mulHeight (HPow.hPow (α := ι → K) 0 (n + 1)) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ (n + 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
⊢ Nonempty ι

Tactic:
have : Nonempty ι := (ne_iff.mp hx).nonempty
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
v : AbsoluteValue K ℝ
simp :
  ⨆ (i : ι), HPow.hPow (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) n =
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n
⊢ ⨆ (i : ι), (v : (a : K) → ℝ) ((x ^ n) i) = HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n

Tactic:
simp only [Pi.pow_apply, map_pow]

Premises used: map_pow, Pi.pow_apply
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
v : AbsoluteValue K ℝ
simp :
  ⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ) ^ n =
    HPow.hPow (α := ℝ) (⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ)) n
⊢ ⨆ (i : ι), HPow.hPow (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) n =
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n

Tactic:
simp +singlePass only [← coe_toNNReal _ (v.nonneg _)]

Premises used: AbsoluteValue.nonneg, Real.coe_toNNReal
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
v : AbsoluteValue K ℝ
norm_cast :
  ⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i)) ^ n =
    HPow.hPow (α := NNReal) (⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i))) n
⊢ ⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ) ^ n =
    HPow.hPow (α := ℝ) (⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ)) n

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
v : AbsoluteValue K ℝ
⊢ ⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i)) ^ n =
    HPow.hPow (α := NNReal) (⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i))) n

Tactic:
(pow_left_mono n).map_ciSup_of_continuousAt (continuous_pow n).continuousAt
      (Finite.bddAbove_range _) |>.symm

Premises used: pow_left_mono, Monotone.map_ciSup_of_continuousAt, Continuous.continuousAt, Finite.bddAbove_range, Eq.symm, continuous_pow
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
v : AbsoluteValue K ℝ
⊢ ⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i)) ^ n =
    HPow.hPow (α := NNReal) (⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i))) n

Tactic:
exact (pow_left_mono n).map_ciSup_of_continuousAt (continuous_pow n).continuousAt
      (Finite.bddAbove_range _) |>.symm

Premises used: pow_left_mono, Monotone.map_ciSup_of_continuousAt, Continuous.continuousAt, Finite.bddAbove_range, Eq.symm, continuous_pow
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
⊢ ∀ (v : AbsoluteValue K ℝ),
    ⨆ (i : ι), (v : (a : K) → ℝ) ((x ^ n) i) = HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n

Tactic:
have H (v : AbsoluteValue K ℝ) : ⨆ i : ι, v ((x ^ n) i) = (⨆ i, v (x i)) ^ n := by
    simp only [Pi.pow_apply, map_pow]
    simp +singlePass only [← coe_toNNReal _ (v.nonneg _)]
    norm_cast
    exact (pow_left_mono n).map_ciSup_of_continuousAt (continuous_pow n).continuousAt
      (Finite.bddAbove_range _) |>.symm
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    ⨆ (i : ι), (v : (a : K) → ℝ) ((x ^ n) i) = HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n
⊢ x ^ n ≠ 0

Tactic:
simp [hx]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    ⨆ (i : ι), (v : (a : K) → ℝ) ((x ^ n) i) = HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n
⊢ x ^ n ≠ 0

Tactic:
have hxn : x ^ n ≠ 0 := by simp [hx]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    ⨆ (i : ι), (v : (a : K) → ℝ) ((x ^ n) i) = HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n
hxn : x ^ n ≠ 0
⊢ mulHeight (x ^ n) = mulHeight x ^ n

Tactic:
simp only [mulHeight_eq hx, mulHeight_eq hxn, H, mul_pow,
    finprod_pow <| hasFiniteMulSupport_iSup_nonarchAbsVal hx, ← Multiset.prod_map_pow]

Premises used: Multiset.prod_map_pow, _private.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal, Height.mulHeight_eq, finprod_pow, mul_pow
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
⊢ logHeight (x ^ n) = (↑n : ℝ) * logHeight x

Tactic:
simp [logHeight_eq_log_mulHeight, mulHeight_pow x n]

Premises used: Height.mulHeight_pow, Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
simp_rw : mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
⊢ mulHeight₁ x⁻¹ = mulHeight₁ x

Tactic:
simp_rw [mulHeight₁_eq_mulHeight]

Premises used: Height.mulHeight₁_eq_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
inl : mulHeight.{u_1, 0} (K := K) ![0⁻¹, 1] = mulHeight.{u_1, 0} (K := K) ![0, 1]
inr : ∀ (hx : x ≠ 0), mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
inl inl₁ : mulHeight.{u_1, 0} (K := K) ![0, 1] = mulHeight.{u_1, 0} (K := K) ![0, 1]
⊢ mulHeight.{u_1, 0} (K := K) ![0⁻¹, 1] = mulHeight.{u_1, 0} (K := K) ![0, 1]

Tactic:
rw [inv_zero]

Premises used: inv_zero
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
h : ∀ (i : Fin (Nat.succ 0).succ), (x • ![x⁻¹, 1]) i = ![1, x] i
⊢ x • ![x⁻¹, 1] = ![1, x]

Tactic:
ext1 i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
i : Fin (Nat.succ 0).succ
h :
  (x • ![x⁻¹, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![1, x] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  (x • ![x⁻¹, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![1, x] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (x • ![x⁻¹, 1]) i = ![1, x] i

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![1, x] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hx]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![1, x] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hx]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ x • ![x⁻¹, 1] = ![1, x]

Tactic:
have H : x • ![x⁻¹, 1] = ![1, x] := by ext1 i; fin_cases i <;> simp [hx]
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
H : x • ![x⁻¹, 1] = ![1, x]
inr : mulHeight (x • ![x⁻¹, 1]) = mulHeight ![x, 1]
inr₁ : mulHeight ![1, x] = mulHeight ![x, 1]
inr₂ inr₃ : mulHeight ![x, 1] = mulHeight ![x, 1]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]

Tactic:
rw [← mulHeight_smul_eq_mulHeight _ hx, H, mulHeight_swap]

Premises used: Height.mulHeight_swap, Height.mulHeight_smul_eq_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ logHeight₁ x⁻¹ = logHeight₁ x

Tactic:
simp only [logHeight₁_eq_log_mulHeight₁, mulHeight₁_inv]

Premises used: Height.mulHeight₁_inv, Height.logHeight₁_eq_log_mulHeight₁
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
simp : mulHeight ![x ^ n, 1] = mulHeight (![x, 1] ^ n)
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n

Tactic:
simp only [mulHeight₁_eq_mulHeight, ← mulHeight_pow _ n]

Premises used: Height.mulHeight_pow, Height.mulHeight₁_eq_mulHeight
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
e_x : ![x ^ n, 1] = ![x, 1] ^ n
⊢ mulHeight ![x ^ n, 1] = mulHeight (![x, 1] ^ n)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
e_x : ∀ (i : Fin (Nat.succ 0).succ), ![x ^ n, 1] i = (![x, 1] ^ n) i
⊢ ![x ^ n, 1] = ![x, 1] ^ n

Tactic:
ext1 i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
i : Fin (Nat.succ 0).succ
e_x :
  ![x ^ n, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] ^ n) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
e_x₁ :
  ![x ^ n, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] ^ n) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![x ^ n, 1] i = (![x, 1] ^ n) i

Tactic:
fin_cases i
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    (![x, 1] ^ n) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp