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
inst_2 : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
inr :
  HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
        (Multiset.prod
          (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal)) *
      ∏ᶠ (v : (↑nonarchAbsVal : Type u_1)),
        HMul.hMul (α := ℝ) (β := ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) c : ℝ)
          (⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i) : ℝ) =
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))
⊢ mulHeight (c • x) = mulHeight x

Tactic:
simp only [mulHeight_eq hx, mulHeight_eq hcx, Pi.smul_apply, smul_eq_mul, map_mul,
    ← mul_iSup_of_nonneg <| AbsoluteValue.nonneg .., Multiset.prod_map_mul]

Premises used: Multiset.prod_map_mul, AbsoluteValue.nonneg, Height.mulHeight_eq, map_mul, smul_eq_mul, Real.mul_iSup_of_nonneg, Pi.smul_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
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
funProp : c ≠ 0
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦ ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) c

Tactic:
fun_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
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
funProp : x ≠ 0
⊢ HasFiniteMulSupport (M := ℝ) fun (v : (↑nonarchAbsVal : Type u_1)) ↦
    ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i)

Tactic:
fun_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
inl : 1 ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
inr : ∀ (hx : x ≠ 0), 1 ≤ mulHeight x
⊢ 1 ≤ mulHeight x

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 ι
⊢ 1 ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 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 ι
x : ι → K
hx : x ≠ 0
⊢ ∃ (i : ι), x i ≠ 0

Tactic:
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_2
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
inr : ∀ (i : ι) (hi : x i ≠ 0), 1 ≤ mulHeight x
⊢ 1 ≤ mulHeight x

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := 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_2
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
⊢ (x i)⁻¹ • x ≠ 0

Tactic:
simp [hi, 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
⊢ (x i)⁻¹ • x ≠ 0

Tactic:
have hx' : (x i)⁻¹ • x ≠ 0 := by simp [hi, 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
inr :
  1 ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (v : (a : K) → ℝ) (((x i)⁻¹ • x) i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))
⊢ 1 ≤ mulHeight x

Tactic:
rw [← mulHeight_smul_eq_mulHeight _ <| inv_ne_zero hi, mulHeight_eq hx']

Premises used: Height.mulHeight_smul_eq_mulHeight, Height.mulHeight_eq, inv_ne_zero
-- 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
⊢ 1 ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (v : (a : K) → ℝ) (((x i)⁻¹ • x) i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))

Tactic:
one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod_map fun v _ ↦ ?_) ?_

Premises used: Multiset.one_le_prod_map, one_le_mul_of_one_le_of_one_le
-- 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
inr :
  ∀ (v : AbsoluteValue K ℝ),
    Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v →
      LE.le (α := ℝ) 1 (⨆ (i_1 : ι), (v : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))
inr₁ :
  LE.le (α := ℝ) 1
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))
⊢ 1 ≤
    HMul.hMul (α := ℝ)
      (Multiset.prod
        (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (v : (a : K) → ℝ) (((x i)⁻¹ • x) i_1)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))

Tactic:
refine one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod_map fun v _ ↦ ?_) ?_

Premises used: Multiset.one_le_prod_map, one_le_mul_of_one_le_of_one_le
-- 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
⊢ LE.le (α := ℝ) 1 (⨆ (i_1 : ι), (v : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))

Tactic:
Finite.le_ciSup_of_le i <| le_of_eq ?_

Premises used: Finite.le_ciSup_of_le, le_of_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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
inr : Eq (α := ℝ) (1 : ℝ) ((v : (a : K) → ℝ) (((x i)⁻¹ • x) i) : ℝ)
⊢ LE.le (α := ℝ) 1 (⨆ (i_1 : ι), (v : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))

Tactic:
refine Finite.le_ciSup_of_le i <| le_of_eq ?_

Premises used: Finite.le_ciSup_of_le, le_of_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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : AbsoluteValue K ℝ
h : Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v
⊢ Eq (α := ℝ) (1 : ℝ) ((v : (a : K) → ℝ) (((x i)⁻¹ • x) i) : ℝ)

Tactic:
simpa using (inv_mul_cancel₀ <| v.ne_zero_iff.mpr hi).symm

Premises used: Iff.mpr, AbsoluteValue.ne_zero_iff, Eq.symm, inv_mul_cancel₀
-- 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
⊢ LE.le (α := ℝ) 1
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))

Tactic:
one_le_finprod fun v ↦ Finite.le_ciSup_of_le i ?_

Premises used: one_le_finprod, 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
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
inr :
  ∀ (v : (↑nonarchAbsVal : Type u_1)),
    LE.le (α := ℝ) (1 : ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i) : ℝ)
⊢ LE.le (α := ℝ) 1
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i_1))

Tactic:
refine one_le_finprod fun v ↦ Finite.le_ciSup_of_le i ?_

Premises used: one_le_finprod, 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
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
v : (↑nonarchAbsVal : Type u_1)
⊢ LE.le (α := ℝ) (1 : ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i) : ℝ)

Tactic:
simp [inv_mul_cancel₀ <| v.val.ne_zero_iff.mpr hi]

Premises used: Iff.mpr, AbsoluteValue.ne_zero_iff, Subtype.val, inv_mul_cancel₀
-- 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
⊢ 0 < mulHeight x

Tactic:
zero_lt_one.trans_le <| one_le_mulHeight x

Premises used: Height.one_le_mulHeight, zero_lt_one, LT.lt.trans_le
-- 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
⊢ mulHeight x ≠ 0

Tactic:
(mulHeight_pos x).ne'

Premises used: Height.mulHeight_pos, LT.lt.ne'
-- 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
⊢ 0 ≤ logHeight x

Tactic:
log_nonneg <| one_le_mulHeight x

Premises used: Height.one_le_mulHeight, Height.logHeight, Real.log_nonneg
-- 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 ι'
f : ι → ι'
x : ι' → K
inl : ∀ (h₀ : x ∘ f = 0), mulHeight (x ∘ f) ≤ mulHeight x
inr : ∀ (h₀ : x ∘ f ≠ 0), mulHeight (x ∘ f) ≤ mulHeight x
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
rcases eq_or_ne (x ∘ f) 0 with h₀ | h₀

Premises used: Function.comp, eq_or_ne, OfNat.ofNat
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f = 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
simpa [h₀] using one_le_mulHeight _

Premises used: Height.one_le_mulHeight
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
inr :
  ∀ (h₀ : Ne (α := ι → K) (0 ∘ f) 0), mulHeight.{u_1, u_2} (K := K) (0 ∘ f) ≤ mulHeight.{u_1, u_3} (K := K) (ι := ι') 0
inr₁ : ∀ (hx : x ≠ 0), mulHeight (x ∘ f) ≤ mulHeight x
⊢ mulHeight (x ∘ f) ≤ mulHeight x

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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
f : ι → ι'
h₀ : Ne (α := ι → K) (0 ∘ f) 0
⊢ mulHeight.{u_1, u_2} (K := K) (0 ∘ f) ≤ mulHeight.{u_1, u_3} (K := K) (ι := ι') 0

Tactic:
simp
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
⊢ Nonempty ι

Tactic:
have : Nonempty ι := .intro (ne_iff.mp h₀).choose
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
inr :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) 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))
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
rw [mulHeight_eq h₀, mulHeight_eq hx]

Premises used: Height.mulHeight_eq
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))

Tactic:
have H (v : AbsoluteValue K ℝ) : ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i) :=
    ciSup_le fun i ↦ Finite.le_ciSup_of_le (f i) le_rfl
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
inr :
  LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))
inr₁ :
  LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))
inr₂ :
  LE.le (α := ℝ)
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) archAbsVal))
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))
inr₃ :
  LE.le (α := ℝ) (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))
    (∏ᶠ (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) → ℝ) ((x ∘ f) i)) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) 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:
gcongr
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))

Tactic:
finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _

Premises used: finprod_nonneg, Function.comp, Real.iSup_nonneg_of_nonnegHomClass, 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ) 0
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))

Tactic:
exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _

Premises used: finprod_nonneg
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))

Tactic:
Multiset.prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Multiset.prod_map_nonneg, 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ) 0
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))

Tactic:
exact Multiset.prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _

Premises used: Multiset.prod_map_nonneg, 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ)
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) archAbsVal))
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))

Tactic:
Multiset.prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _)
      fun v _ ↦ H v

Premises used: Function.comp, Multiset.prod_map_le_prod_map₀, 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ)
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) archAbsVal))
    (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))

Tactic:
exact Multiset.prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _)
      fun v _ ↦ H v

Premises used: Multiset.prod_map_le_prod_map₀, 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ) (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))

Tactic:
finprod_le_finprod (hasFiniteMulSupport_iSup_nonarchAbsVal h₀)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _)
      (hasFiniteMulSupport_iSup_nonarchAbsVal hx) fun v ↦ H v.val

Premises used: Function.comp, _private.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal, finprod_le_finprod, Real.iSup_nonneg_of_nonnegHomClass, 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H :
  ∀ (v : AbsoluteValue K ℝ),
    LE.le (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) ((x ∘ f) i)) (⨆ (i : ι'), (v : (a : K) → ℝ) (x i))
⊢ LE.le (α := ℝ) (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι'), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i))

Tactic:
exact finprod_le_finprod (hasFiniteMulSupport_iSup_nonarchAbsVal h₀)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _)
      (hasFiniteMulSupport_iSup_nonarchAbsVal hx) fun v ↦ H v.val

Premises used: Function.comp, _private.0.Height.hasFiniteMulSupport_iSup_nonarchAbsVal, finprod_le_finprod, Real.iSup_nonneg_of_nonnegHomClass, 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 ι'
f : ι → ι'
x : ι' → K
⊢ logHeight (x ∘ f) ≤ logHeight x

Tactic:
simpa [logHeight_eq_log_mulHeight] using log_le_log (mulHeight_pos _) <| mulHeight_comp_le ..

Premises used: Height.mulHeight_comp_le, Height.mulHeight_pos, Real.log_le_log, 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
inl : mulHeight (K := K) (ι := ι ⊕ ι') (Sum.elim 0 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
inr : ∀ (hx : x ≠ 0), mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x

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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
⊢ mulHeight (K := K) (ι := ι ⊕ ι') (Sum.elim 0 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0

Tactic:
simp
-- 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
inr : ∀ (i : ι) (hi : x i ≠ 0 i), mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x

Tactic:
obtain ⟨i, hi⟩ := 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_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
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_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ Sum.elim.{u_2, u_3, u_1 + 1} (β := ι') x 0 (Sum.inl i) ≠ 0 (Sum.inl i)

Tactic:
simpa using hi
-- 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 ι
⊢ Ne (α := ι ⊕ ι' → K) (Sum.elim x 0) 0

Tactic:
have hx' : Sum.elim x (0 : ι' → K) ≠ 0 := ne_iff.mpr ⟨.inl i, by simpa using hi⟩
-- 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
inr :
  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))
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x

Tactic:
rw [mulHeight_eq hx, mulHeight_eq hx']

Premises used: Height.mulHeight_eq