awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.Basic
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 ℝ
⊢ Eq (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
le_antisymm ?_ <| ciSup_le fun i ↦ Finite.le_ciSup_of_le (.inl i) le_rfl

Premises used: le_rfl, Sum.inl, le_antisymm, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.Basic
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 ℝ
refine : LE.le (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ Eq (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
refine le_antisymm ?_ <| ciSup_le fun i ↦ Finite.le_ciSup_of_le (.inl i) le_rfl

Premises used: le_antisymm, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.Basic
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 ℝ
⊢ LE.le (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
ciSup_le fun j ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.NumberTheory.Height.Basic
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 ℝ
refine :
  ∀ (j : ι ⊕ ι'), LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 j) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
⊢ LE.le (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
refine ciSup_le fun j ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.NumberTheory.Height.Basic
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_1 : ι
hi : x i_1 ≠ 0 i_1
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
v : AbsoluteValue K ℝ
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) : ℝ)

Tactic:
Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.Basic
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_1 : ι
hi : x i_1 ≠ 0 i_1
this : Nonempty ι
hx' : Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0
v : AbsoluteValue K ℝ
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) : ℝ)

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

Premises used: le_rfl, Finite.le_ciSup_of_le
-- Module: Mathlib.NumberTheory.Height.Basic
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 ℝ
val : ι'
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 (Sum.inr val)) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)

Tactic:
simpa using Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.Basic
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) : ℝ)
inr :
  ∀ (val : ι'),
    LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 (Sum.inr val)) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 j) : ℝ) (⨆ (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 _

Premises used: le_rfl, Finite.le_ciSup_of_le, Real.iSup_nonneg_of_nonnegHomClass
-- Module: Mathlib.NumberTheory.Height.Basic
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 ℝ),
    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 _
-- Module: Mathlib.NumberTheory.Height.Basic
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)
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)
⊢ 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))

Tactic:
congr
-- Module: Mathlib.NumberTheory.Height.Basic
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 :
  ∀ (v : AbsoluteValue K ℝ),
    Eq (α := ℝ) (⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
⊢ 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:
ext1 v
-- Module: Mathlib.NumberTheory.Height.Basic
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 :
  ∀ (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))
⊢ 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:
ext1 v
-- Module: Mathlib.NumberTheory.Height.Basic
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))
v : AbsoluteValue K ℝ
⊢ Eq (α := ℝ) (⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
H v
-- Module: Mathlib.NumberTheory.Height.Basic
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))
v : AbsoluteValue K ℝ
⊢ Eq (α := ℝ) (⨆ (i : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 i)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
exact H v
-- Module: Mathlib.NumberTheory.Height.Basic
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))
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:
H v.val

Premises used: Subtype.val
-- Module: Mathlib.NumberTheory.Height.Basic
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))
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:
exact H v.val

Premises used: Subtype.val
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ logHeight (ι := ι ⊕ ι') (Sum.elim x 0) = logHeight x

Tactic:
congrArg log <| mulHeight_sumElim_zero_eq ..

Premises used: congrArg, Real.log, Height.logHeight, Height.mulHeight_sumElim_zero_eq
-- 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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
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
⊢ 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:
ext1 i
-- 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
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 :
  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
⊢ (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]

Premises used: Function.comp_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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
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:
simp [e]
-- 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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
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:
notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop

Premises used: Function.notMem_support, Subtype.prop, Iff.mp, Set.mem_compl_iff, Sum.elim
-- 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
e : (↑(support x) : Type u_2) ⊕ (↑(support x)ᶜ : Type u_2) ≃ ι := Equiv.Set.sumCompl (support x)
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:
exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop

Premises used: Function.notMem_support, Subtype.prop, Iff.mp, Set.mem_compl_iff
-- 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
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)
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)
⊢ 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:
cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop

Premises used: Function.notMem_support, Iff.mp
-- 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
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)

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
-- 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
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)
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 : ι)
⊢ mulHeight x = mulHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)

Tactic:
rw [← mulHeight_comp_equiv e, hx]

Premises used: Height.mulHeight_comp_equiv
-- 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
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.{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:
mulHeight_sumElim_zero_eq ..

Premises used: Height.mulHeight_sumElim_zero_eq
-- 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
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.{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:
exact mulHeight_sumElim_zero_eq ..

Premises used: Height.mulHeight_sumElim_zero_eq
-- 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
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 : ι)
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 : ι)
⊢ 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 ..

Premises used: Height.mulHeight_sumElim_zero_eq
-- 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
⊢ logHeight x = logHeight.{u_1, u_2} (K := K) fun (i : (↑(support x) : Type u_2)) ↦ x (↑i : ι)

Tactic:
congrArg log <| mulHeight_eq_mulHeight_restrict_support x

Premises used: congrArg, Height.mulHeight_eq_mulHeight_restrict_support, Real.log, Height.logHeight
-- Module: Mathlib.NumberTheory.Height.Basic
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
inr : ∀ (hx : x ≠ 0), 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
ι : Type u_5
inst_2 : Subsingleton ι
⊢ mulHeight.{u_1, u_5} (K := K) (ι := ι) 0 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
hx : x ≠ 0
inr : ∀ (i : ι) (hi : x i ≠ 0 i), mulHeight x = 1
⊢ mulHeight x = 1

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp hx

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Height.Basic
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
⊢ Nonempty ι

Tactic:
have : Nonempty ι := .intro i
-- Module: Mathlib.NumberTheory.Height.Basic
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 ι
inr : mulHeight ((x i)⁻¹ • x) = 1
⊢ mulHeight x = 1

Tactic:
rw [← mulHeight_smul_eq_mulHeight x (inv_ne_zero hi)]

Premises used: Height.mulHeight_smul_eq_mulHeight, inv_ne_zero
-- Module: Mathlib.NumberTheory.Height.Basic
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.{u_1, u_5} (K := K) (ι := ι) 1 = 1

Tactic:
mulHeight_one

Premises used: Height.mulHeight_one
-- Module: Mathlib.NumberTheory.Height.Basic
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 ι
h : (x i)⁻¹ • x = 1
⊢ mulHeight ((x i)⁻¹ • x) = 1

Tactic:
convert! mulHeight_one

Premises used: Height.mulHeight_one
-- Module: Mathlib.NumberTheory.Height.Basic
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 ι
h : ∀ (j : ι), ((x i)⁻¹ • x) j = 1 j
⊢ (x i)⁻¹ • x = 1

Tactic:
ext1 j
-- Module: Mathlib.NumberTheory.Height.Basic
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 ι
j : ι
⊢ ((x i)⁻¹ • x) j = 1 j

Tactic:
simpa [Subsingleton.elim j i] using inv_mul_cancel₀ hi

Premises used: Subsingleton.elim, inv_mul_cancel₀
-- Module: Mathlib.NumberTheory.Height.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
ι : Type u_5
inst_2 : Subsingleton ι
x : ι → K
⊢ logHeight x = 0

Tactic:
simp [logHeight_eq_log_mulHeight]

Premises used: Height.logHeight_eq_log_mulHeight