awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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])
⊢ logHeight₁ (x / y) = logHeight ![x, y]
have rw₂ : log (mulHeight ![x, y]) = log (mulHeight ![x, y])
Tactic: rw [logHeight₁_eq_log_mulHeight₁, logHeight_eq_log_mulHeight, mulHeight₁_div_eq_mulHeight x y]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
⊢ mulHeight (x ^ n) = mulHeight x ^ n
have inl : mulHeight (HPow.hPow (α := ι → K) 0 n) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ n
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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
⊢ mulHeight (x ^ n) = mulHeight x ^ n
have inr : ∀ (hx : x ≠ 0), mulHeight (x ^ n) = mulHeight x ^ n
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ n
have inl : mulHeight (HPow.hPow (α := ι → K) (β := ℕ) 0 0) = HPow.hPow (β := ℕ) (mulHeight.{u_1, u_2} (K := K) (ι := ι) 0) 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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
⊢ mulHeight (HPow.hPow (α := ι → K) 0 n) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ n
have inl₁ : ∀ (n : ℕ), mulHeight (HPow.hPow (α := ι → K) 0 (n + 1)) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0 ^ (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
inst_2 : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
⊢ mulHeight (x ^ n) = mulHeight x ^ n
have this : Nonempty ι
Tactic: have : Nonempty ι := (ne_iff.mp hx).nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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
have simp : ⨆ (i : ι), HPow.hPow (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) n =
  HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n
Tactic: simp only [Pi.pow_apply, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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 : ι), HPow.hPow (α := ℝ) ((v : (a : K) → ℝ) (x i) : ℝ) n =
    HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) n
have simp : ⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ) ^ n =
  HPow.hPow (α := ℝ) (⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ)) n
Tactic: simp +singlePass only [← coe_toNNReal _ (v.nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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 (α := ℝ) (⨆ (i : ι), (↑(toNNReal ((v : (a : K) → ℝ) (x i))) : ℝ)) n
have norm_cast : ⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i)) ^ n =
  HPow.hPow (α := NNReal) (⨆ (i : ι), toNNReal ((v : (a : K) → ℝ) (x i))) n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
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 ι
⊢ mulHeight (x ^ n) = mulHeight x ^ n
have H : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
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
⊢ mulHeight (x ^ n) = mulHeight x ^ n
have hxn : x ^ n ≠ 0
Tactic: have hxn : x ^ n ≠ 0 := by simp [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x⁻¹ = mulHeight₁ x
have simp_rw : mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
Tactic: simp_rw [mulHeight₁_eq_mulHeight]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
have inl : mulHeight.{u_1, 0} (K := K) ![0⁻¹, 1] = mulHeight.{u_1, 0} (K := K) ![0, 1]
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
have inr : ∀ (hx : x ≠ 0), mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
⊢ mulHeight.{u_1, 0} (K := K) ![0⁻¹, 1] = mulHeight.{u_1, 0} (K := K) ![0, 1]
have inl : mulHeight.{u_1, 0} (K := K) ![0, 1] = mulHeight.{u_1, 0} (K := K) ![0, 1]
Tactic: rw [inv_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ x • ![x⁻¹, 1] = ![1, x]
have h : ∀ (i : Fin (Nat.succ 0).succ), (x • ![x⁻¹, 1]) i = ![1, x] i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
i : Fin (Nat.succ 0).succ
⊢ (x • ![x⁻¹, 1]) i = ![1, x] i
have h : (x • ![x⁻¹, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
  ![1, x] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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, ⋯⟩)
⊢ (x • ![x⁻¹, 1]) i = ![1, x] i
have h₁ : (x • ![x⁻¹, 1]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
  ![1, x] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
have H : x • ![x⁻¹, 1] = ![1, x]
Tactic: have H : x • ![x⁻¹, 1] = ![1, x] := by ext1 i; fin_cases i <;> simp [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
hx : x ≠ 0
H : x • ![x⁻¹, 1] = ![1, x]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
have inr : mulHeight (x • ![x⁻¹, 1]) = mulHeight ![x, 1]
Tactic: rw [← mulHeight_smul_eq_mulHeight _ hx, H, mulHeight_swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
have inr₁ : mulHeight ![1, x] = mulHeight ![x, 1]
Tactic: rw [← mulHeight_smul_eq_mulHeight _ hx, H, mulHeight_swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
have inr₂ : mulHeight ![x, 1] = mulHeight ![x, 1]
Tactic: rw [← mulHeight_smul_eq_mulHeight _ hx, H, mulHeight_swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n
have simp : mulHeight ![x ^ n, 1] = mulHeight (![x, 1] ^ n)
Tactic: simp only [mulHeight₁_eq_mulHeight, ← mulHeight_pow _ n]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight ![x ^ n, 1] = mulHeight (![x, 1] ^ n)
have e_x : ![x ^ n, 1] = ![x, 1] ^ n
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] = ![x, 1] ^ n
have e_x : ∀ (i : Fin (Nat.succ 0).succ), ![x ^ n, 1] i = (![x, 1] ^ n) i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
i : Fin (Nat.succ 0).succ
⊢ ![x ^ n, 1] i = (![x, 1] ^ n) i
have e_x : ![x ^ n, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
  (![x, 1] ^ n) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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, ⋯⟩)
⊢ ![x ^ n, 1] i = (![x, 1] ^ n) i
have e_x₁ : ![x ^ n, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
  (![x, 1] ^ n) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
have inl : ∀ (h : 0 ≤ n), mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
Tactic: rcases le_or_gt 0 n with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
inl : ∀ (h : 0 ≤ n), mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
have inr : ∀ (h : n < 0), mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
Tactic: rcases le_or_gt 0 n with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : 0 ≤ n
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
have inl : ∀ (n : ℕ), mulHeight₁ (HPow.hPow (β := ℤ) x (↑n : ℤ)) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
Tactic: lift n to ℕ using h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (↑n : ℤ)) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
have inl : mulHeight₁ (x ^ n) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
Tactic: rw [zpow_natCast, mulHeight₁_pow, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
inl : mulHeight₁ (x ^ n) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (↑n : ℤ)) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
have inl₁ : mulHeight₁ x ^ n = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
Tactic: rw [zpow_natCast, mulHeight₁_pow, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℕ
inl : mulHeight₁ (x ^ n) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
inl₁ : mulHeight₁ x ^ n = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (↑n : ℤ)) = mulHeight₁ x ^ Int.natAbs (↑n : ℤ)
have inl₂ : mulHeight₁ x ^ n = mulHeight₁ x ^ n
Tactic: rw [zpow_natCast, mulHeight₁_pow, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
have inr : mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs
Tactic: nth_rewrite 1 [show n = -n.natAbs by grind]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs
have inr : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = mulHeight₁ x ^ n.natAbs
Tactic: rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
inr : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs
have inr₁ : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ)) = mulHeight₁ x ^ n.natAbs
Tactic: rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
inr : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = mulHeight₁ x ^ n.natAbs
inr₁ : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ)) = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs
have inr₂ : mulHeight₁ (x ^ n.natAbs) = mulHeight₁ x ^ n.natAbs
Tactic: rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
inr : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ))⁻¹ = mulHeight₁ x ^ n.natAbs
inr₁ : mulHeight₁ (HPow.hPow (β := ℤ) x (↑n.natAbs : ℤ)) = mulHeight₁ x ^ n.natAbs
inr₂ : mulHeight₁ (x ^ n.natAbs) = mulHeight₁ x ^ n.natAbs
⊢ mulHeight₁ (HPow.hPow (β := ℤ) x (-(↑n.natAbs : ℤ))) = mulHeight₁ x ^ n.natAbs
have inr₃ : mulHeight₁ x ^ n.natAbs = mulHeight₁ x ^ n.natAbs
Tactic: rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = ∏ a : α, mulHeight (x a)
have rw : HMul.hMul (α := ℝ)
    (Multiset.prod
      (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : (a : α) → ι a), (v : (a : K) → ℝ) (∏ a : α, x a (i a)))
        archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
      ⨆ (i : (a : α) → ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∏ a : α, x a (i a))) =
  ∏ a : α, mulHeight (x a)
Tactic: rw [mulHeight_eq ?h₁]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
rw :
  HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : (a : α) → ι a), (v : (a : K) → ℝ) (∏ a : α, x a (i a)))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : (a : α) → ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∏ a : α, x a (i a))) =
    ∏ a : α, mulHeight (x a)
⊢ (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = ∏ a : α, mulHeight (x a)
have rw₁ : Ne (α := ((a : α) → ι a) → K) (fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) 0
Tactic: rw [mulHeight_eq ?h₁]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ Ne (α := ((a : α) → ι a) → K) (fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) 0
have simp_rw : ∀ (hx : ∀ (a : α), ∃ (a_1 : ι a), x a a_1 ≠ 0),
  ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0
Tactic: simp_rw [ne_iff, Pi.zero_def] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), ∃ (a_1 : ι a), x a a_1 ≠ 0
⊢ ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0
have choose : ∀ (f : (a : α) → ι a) (hf : ∀ (a : α), x a (f a) ≠ 0),
  ∃ (a : (a : α) → ι a), Ne.{u_1 + 1} (α := K) (∏ a_1 : α, x a_1 (a a_1)) 0
Tactic: choose f hf using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : (a : α) → ι a), (v : (a : K) → ℝ) (∏ a : α, x a (i a)))
          archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : (a : α) → ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (∏ a : α, x a (i a))) =
    ∏ a : α, mulHeight (x a)
have simp_rw : HMul.hMul (α := ℝ)
    (Multiset.prod
      (Multiset.map (fun (x_1 : AbsoluteValue K ℝ) ↦ ∏ a : α, ⨆ (i : ι a), (x_1 : (a : K) → ℝ) (x a i)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ∏ a : α, ⨆ (i : ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
  ∏ a : α, mulHeight (x a)
Tactic: simp_rw [_root_.map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (x_1 : AbsoluteValue K ℝ) ↦ ∏ a : α, ⨆ (i : ι a), (x_1 : (a : K) → ℝ) (x a i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ∏ a : α, ⨆ (i : ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
    ∏ a : α, mulHeight (x a)
have rw : Eq (α := ℝ)
  (∏ x_1 : α,
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι x_1), (i : (a : K) → ℝ) (x x_1 i_1)) archAbsVal))
      (∏ᶠ (a : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι x_1), ((↑a : AbsoluteValue K ℝ) : (a : K) → ℝ) (x x_1 i)))
  (∏ a : α, mulHeight (x a))
Tactic: rw [Multiset.prod_map_prod,
    finprod_prod_comm _ _ fun b _ ↦ hasFiniteMulSupport_iSup_nonarchAbsVal (hx b),
    ← prod_mul_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
a : α
h : Membership.mem (γ := Finset α) univ a
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι a), (i : (a : K) → ℝ) (x a i_1)) archAbsVal))
      (∏ᶠ (a_1 : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι a), ((↑a_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
    mulHeight (x a)
have rw : HMul.hMul (α := ℝ)
    (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι a), (i : (a : K) → ℝ) (x a i_1)) archAbsVal))
    (∏ᶠ (a_1 : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι a), ((↑a_1 : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i)) =
  HMul.hMul (α := ℝ)
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι a), (v : (a : K) → ℝ) (x a i)) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι a), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x a i))
Tactic: rw [mulHeight_eq (hx a)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
α : Type u
inst_2 : Fintype α
ι : α → Type v
inst_3 : ∀ (a : α), Finite.{v + 1} (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ log (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = ∑ x_1 : α, log (mulHeight (x x_1))
have rw : log (mulHeight (K := K) fun (I : (a : α) → ι a) ↦ ∏ a : α, x a (I a)) = log (∏ i : α, mulHeight (x i))
Tactic: rw [← log_prod fun a _ ↦ mulHeight_ne_zero _]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
have obtain : ∀ (i : ι) (hi : x i ≠ 0 i), Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
Tactic: obtain ⟨i, hi⟩ := ne_iff.mp hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
i : ι
hi : x i ≠ 0 i
⊢ Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
have obtain : ∀ (j : ι') (hj : y j ≠ 0 j), Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
Tactic: obtain ⟨j, hj⟩ := ne_iff.mp hy
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
⊢ (mulHeight (K := K) fun (a : ι × ι') ↦ x a.1 * y a.2) = mulHeight x * mulHeight y
have hxy : Ne (α := (a : ι × ι') → K) (fun (a : ι × ι') ↦ x a.1 * y a.2) 0
Tactic: have hxy : (fun a : ι × ι' ↦ x a.1 * y a.2) ≠ 0 := by
    obtain ⟨i, hi⟩ := ne_iff.mp hx
    obtain ⟨j, hj⟩ := ne_iff.mp hy
    exact ne_iff.mpr ⟨⟨i, j⟩, mul_ne_zero hi hj⟩