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
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
v : AbsoluteValue K ℝ
j : ι ⊕ ι'
inl :
  ∀ (i : ι),
    LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim.{u_2, u_3, u_1 + 1} (β := ι') x 0 (Sum.inl i)) : ℝ)
      (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 j) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
have inr : ∀ (val : ι'),
  LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 (Sum.inr val)) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
Tactic: cases j with
    | inl i => exact Finite.le_ciSup_of_le i le_rfl
    | inr _ => simpa using Real.iSup_nonneg_of_nonnegHomClass v _
Cleared hypotheses: j
-- 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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι ⊕ ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (Sum.elim x 0 i)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
have H : ∀ (v : AbsoluteValue K ℝ),
  Eq (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
Tactic: have H (v : AbsoluteValue K ℝ) : ⨆ j, v (Sum.elim x (0 : ι' → K) j) = ⨆ i, v (x i) := by
    refine le_antisymm ?_ <| ciSup_le fun i ↦ Finite.le_ciSup_of_le (.inl i) le_rfl
    refine ciSup_le fun j ↦ ?_
    cases j with
    | inl i => exact Finite.le_ciSup_of_le i le_rfl
    | inr _ => simpa using Real.iSup_nonneg_of_nonnegHomClass v _
-- 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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι ⊕ ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (Sum.elim x 0 i)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
have inr : Eq.{u_1 + 1} (α := AbsoluteValue K ℝ → ℝ)
  (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) fun (v : AbsoluteValue K ℝ) ↦
  ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
Tactic: congr
-- 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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
inr :
  Eq.{u_1 + 1} (α := AbsoluteValue K ℝ → ℝ)
    (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) fun (v : AbsoluteValue K ℝ) ↦
    ⨆ (i : ι), (v : (a : K) → ℝ) (x i)
⊢ HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        ⨆ (i : ι ⊕ ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (Sum.elim x 0 i)) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) (x i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
have inr₁ : Eq.{u_1 + 1} (α := (↑nonarchAbsVal : Type u_1) → ℝ)
  (fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ⨆ (i : ι ⊕ ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (Sum.elim x 0 i))
  fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
Tactic: congr
-- 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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
H :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ Eq.{u_1 + 1} (α := (↑nonarchAbsVal : Type u_1) → ℝ)
    (fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ⨆ (i : ι ⊕ ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (Sum.elim x 0 i))
    fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)
have inr : ∀ (v : (↑nonarchAbsVal : Type u_1)),
  Eq (α := ℝ) (⨆ (i : ι ⊕ ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (Sum.elim x 0 i))
    (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
Tactic: ext1 v
-- 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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
⊢ Eq (α := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) → K)
    (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι))
    (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0)
have h : ∀ (i : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)),
  (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι)) i =
    Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 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
ι : Type u_2
inst_2 : Finite ι
x : ι → K
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
i : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)
⊢ (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι)) i =
    Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 i
have h : x ((e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι) i) =
  Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 i
Tactic: simp only [comp_apply]
-- 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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
i : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)
⊢ x ((e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι) i) =
    Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 i
have h : ∀ (val : (↑(support x) : Type u_2)),
  x ((e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι) (Sum.inl val)) =
    Sum.elim (β := (↑(support x)ᶜ : Type u_2)) (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 (Sum.inl val)
Tactic: cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
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
ι : Type u_2
inst_2 : Finite ι
x : ι → K
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
i : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)
h :
  ∀ (val : (↑(support x) : Type u_2)),
    x ((e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι) (Sum.inl val)) =
      Sum.elim (β := (↑(support x)ᶜ : Type u_2)) (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 (Sum.inl val)
⊢ x ((e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι) i) =
    Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 i
have h₁ : ∀ (val : (↑(support x)ᶜ : Type u_2)),
  x ((e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι) (Sum.inr val)) =
    Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0 (Sum.inr val)
Tactic: cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
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
ι : Type u_2
inst_2 : Finite ι
x : ι → K
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
⊢ mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
have hx : Eq (α := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) → K)
  (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι))
  (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0)
Tactic: have hx : x ∘ e = Sum.elim (fun i : x.support ↦ x i.val) 0 := by
    ext1 i
    simp only [comp_apply]
    cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
-- 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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
hx :
  Eq (α := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) → K)
    (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι))
    (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0)
⊢ mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
have rw : mulHeight.{u_1, u_2} (K := K) (ι := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2))
    (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0) =
  mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
Tactic: rw [← mulHeight_comp_equiv e, 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 ι
x : ι → K
let let₁ let₂ : mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
⊢ mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
have let₃ : let e := Equiv.Set.sumCompl (support x);
∀
  (hx :
    Eq (α := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) → K)
      (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι))
      (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0)),
  mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
Tactic: classical
  let e := Equiv.Set.sumCompl x.support
  have hx : x ∘ e = Sum.elim (fun i : x.support ↦ x i.val) 0 := by
    ext1 i
    simp only [comp_apply]
    cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
  rw [← mulHeight_comp_equiv e, hx]
  exact mulHeight_sumElim_zero_eq ..
-- 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
let let₁ let₂ : mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
let₃ :
  let e := Equiv.Set.sumCompl (support x);
  ∀
    (hx :
      Eq (α := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) → K)
        (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι))
        (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0)),
    mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
⊢ mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
have let₄ : let e := Equiv.Set.sumCompl (support x);
∀
  (hx :
    Eq (α := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) → K)
      (x ∘ (⇑e : (a : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2)) → ι))
      (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0)),
  mulHeight.{u_1, u_2} (K := K) (ι := (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2))
      (Sum.elim (fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)) 0) =
    mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)
Tactic: classical
  let e := Equiv.Set.sumCompl x.support
  have hx : x ∘ e = Sum.elim (fun i : x.support ↦ x i.val) 0 := by
    ext1 i
    simp only [comp_apply]
    cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop
  rw [← mulHeight_comp_equiv e, hx]
  exact mulHeight_sumElim_zero_eq ..
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
⊢ mulHeight x = 1
have inl : mulHeight.{u_1, u_5} (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
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
inl : mulHeight.{u_1, u_5} (K := K) (ι := ι) 0 = 1
⊢ mulHeight x = 1
have inr : ∀ (hx : x ≠ 0), 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
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
hx : x ≠ 0
⊢ mulHeight x = 1
have inr : ∀ (i : ι) (hi : x i ≠ 0 i), mulHeight x = 1
Tactic: obtain ⟨i, hi⟩ := Function.ne_iff.mp hx
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
⊢ mulHeight x = 1
have this : Nonempty ι
Tactic: have : Nonempty ι := .intro i
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight x = 1
have inr : mulHeight ((x i)⁻¹ • x) = 1
Tactic: rw [← mulHeight_smul_eq_mulHeight x (inv_ne_zero hi)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight ((x i)⁻¹ • x) = 1
have h : (x i)⁻¹ • x = 1
Tactic: convert! mulHeight_one
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ (x i)⁻¹ • x = 1
have h : ∀ (j : ι), ((x i)⁻¹ • x) j = 1 j
Tactic: ext1 j
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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)
have h : ∀ (j : Fin n ⊕ Fin 1), (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) j = Sum.elim x 0 j
Tactic: ext j : 1
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
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 ⋯))
⊢ mulHeight (vecCons 0 x) = mulHeight x
have he : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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)
⊢ mulHeight (vecCons 0 x) = mulHeight x
have rw : mulHeight (ι := Fin n ⊕ Fin 1) (vecCons 0 x ∘ (⇑e : (a : Fin n ⊕ Fin 1) → Fin n.succ)) = mulHeight x
Tactic: rw [← mulHeight_comp_equiv e, he, mulHeight_sumElim_zero_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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
⊢ mulHeight (vecCons 0 x) = mulHeight x
have rw₁ : mulHeight (ι := Fin n ⊕ Fin 1) (Sum.elim x 0) = mulHeight x
Tactic: rw [← mulHeight_comp_equiv e, he, mulHeight_sumElim_zero_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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
⊢ mulHeight (vecCons 0 x) = mulHeight x
have rw₂ : mulHeight x = mulHeight x
Tactic: rw [← mulHeight_comp_equiv e, he, mulHeight_sumElim_zero_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons 0 x)) = mulHeight (vecCons a x)
have 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)
Tactic: rw [← mulHeight_comp_equiv (Equiv.swap 0 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons b (vecCons 0 x))) = mulHeight (vecCons a (vecCons b x))
have 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))
Tactic: rw [← mulHeight_comp_equiv (Equiv.swap (Fin.succ 0) (Fin.succ 1)), ← cons_swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
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 : ℝ)
have 0 : Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))) : ℝ)
  (![(v : (a : K) → ℝ) x, 1] ((fun (i : Fin 2) ↦ 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_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, ⋯⟩) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] i) : ℝ) (![(v : (a : K) → ℝ) x, 1] i : ℝ)
have 1 : Eq (α := ℝ) ((v : (a : K) → ℝ) (![x, 1] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))) : ℝ)
  (![(v : (a : K) → ℝ) x, 1] ((fun (i : Fin 2) ↦ 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_1 : 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) : ℝ)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x = mulHeight ![x, 1]
have 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) : ℝ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
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) : ℝ)
⊢ mulHeight₁ x = mulHeight ![x, 1]
have hx : ![x, 1] ≠ 0
Tactic: have hx : ![x, 1] ≠ 0 := by simp
-- 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
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]
have inl : mulHeight₁ (x / 0) = mulHeight ![x, 0]
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y
-- 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
inl : mulHeight₁ (x / 0) = mulHeight ![x, 0]
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]
have inr : ∀ (hy : y ≠ 0), mulHeight₁ (x / y) = mulHeight ![x, y]
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- 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
hy : y ≠ 0
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]
have inr : mulHeight (y • ![x / y, 1]) = mulHeight ![x, y]
Tactic: rw [mulHeight₁_eq_mulHeight, ← mulHeight_smul_eq_mulHeight _ hy]
-- 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
⊢ logHeight₁ (x / y) = logHeight ![x, y]
have rw : log (mulHeight₁ (x / y)) = logHeight ![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
x y : K
rw : log (mulHeight₁ (x / y)) = logHeight ![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]