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
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)) *
      HMul.hMul (α := ℝ) (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c)
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
    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))
⊢ 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))
have inr₁ : HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
      (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c) *
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
  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))
Tactic: rw [finprod_mul_distrib (by fun_prop) (by fun_prop),
    mul_mul_mul_comm, product_formula hc, one_mul]
-- 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
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)) *
      HMul.hMul (α := ℝ) (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c)
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
    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))
inr₁ :
  HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ (i : (a : K) → ℝ) c) archAbsVal))
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) c) *
      HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
        (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
    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))
⊢ 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))
have inr₂ : 1 *
    HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (i : AbsoluteValue K ℝ) ↦ ⨆ (i_1 : ι), (i : (a : K) → ℝ) (x i_1)) archAbsVal))
      (∏ᶠ (i : (↑nonarchAbsVal : Type u_1)), ⨆ (i_1 : ι), ((↑i : AbsoluteValue K ℝ) : (a : K) → ℝ) (x i_1)) =
  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))
Tactic: rw [finprod_mul_distrib (by fun_prop) (by fun_prop),
    mul_mul_mul_comm, product_formula hc, one_mul]
-- 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
⊢ 1 ≤ mulHeight x
have inl : 1 ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
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
inl : 1 ≤ mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
⊢ 1 ≤ mulHeight x
have inr : ∀ (hx : x ≠ 0), 1 ≤ mulHeight x
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 ι
x : ι → K
hx : x ≠ 0
⊢ 1 ≤ mulHeight x
have inr : ∀ (i : ι) (hi : x i ≠ 0), 1 ≤ mulHeight x
Tactic: obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := 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_2
inst_2 : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
⊢ 1 ≤ mulHeight x
have hx' : (x i)⁻¹ • x ≠ 0
Tactic: have hx' : (x i)⁻¹ • x ≠ 0 := by simp [hi, 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
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
⊢ 1 ≤ mulHeight x
have 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))
Tactic: rw [← mulHeight_smul_eq_mulHeight _ <| inv_ne_zero hi, mulHeight_eq 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
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))
have inr : ∀ (v : AbsoluteValue K ℝ),
  Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) archAbsVal v →
    LE.le (α := ℝ) 1 (⨆ (i_1 : ι), (v : (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 _ ↦ ?_) ?_
-- 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
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))
⊢ 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))
have inr₁ : LE.le (α := ℝ) 1
  (∏ᶠ (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 _ ↦ ?_) ?_
-- 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
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))
have inr : Eq (α := ℝ) (1 : ℝ) ((v : (a : K) → ℝ) (((x i)⁻¹ • x) i) : ℝ)
Tactic: refine Finite.le_ciSup_of_le i <| le_of_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
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))
have inr : ∀ (v : (↑nonarchAbsVal : Type u_1)),
  LE.le (α := ℝ) (1 : ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) (((x i)⁻¹ • x) i) : ℝ)
Tactic: refine one_le_finprod fun v ↦ Finite.le_ciSup_of_le 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
f : ι → ι'
x : ι' → K
⊢ mulHeight (x ∘ f) ≤ mulHeight x
have inl : ∀ (h₀ : x ∘ f = 0), mulHeight (x ∘ f) ≤ mulHeight x
Tactic: rcases eq_or_ne (x ∘ f) 0 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
ι : 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
⊢ mulHeight (x ∘ f) ≤ mulHeight x
have inr : ∀ (h₀ : x ∘ f ≠ 0), mulHeight (x ∘ f) ≤ mulHeight x
Tactic: rcases eq_or_ne (x ∘ f) 0 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
ι : Type u_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x
have inr : ∀ (h₀ : Ne (α := ι → K) (0 ∘ f) 0), mulHeight.{u_1, u_2} (K := K) (0 ∘ f) ≤ mulHeight.{u_1, u_3} (K := K) (ι := ι') 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x, 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_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
⊢ mulHeight (x ∘ f) ≤ mulHeight x
have inr₁ : ∀ (hx : x ≠ 0), mulHeight (x ∘ f) ≤ mulHeight x
Tactic: rcases eq_or_ne x 0 with rfl | 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_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x
have this : Nonempty ι
Tactic: have : Nonempty ι := .intro (ne_iff.mp h₀).choose
-- 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 ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ mulHeight (x ∘ f) ≤ mulHeight x
have 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))
Tactic: rw [mulHeight_eq h₀, mulHeight_eq 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_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ 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))
have H : ∀ (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
-- 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 ι'
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))
⊢ 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))
have inr : LE.le (α := ℝ) 0 (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), ⨆ (i : ι), ((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) ((x ∘ f) i))
Tactic: gcongr
-- 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 ι'
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))
⊢ 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))
have inr₁ : LE.le (α := ℝ) 0
  (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ ⨆ (i : ι'), (v : (a : K) → ℝ) (x i)) archAbsVal))
Tactic: gcongr
-- 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 ι'
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))
⊢ 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))
have 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))
Tactic: gcongr
-- 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 ι'
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))
⊢ 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))
have 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))
Tactic: gcongr
-- 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
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
have inl : mulHeight (K := K) (ι := ι ⊕ ι') (Sum.elim 0 0) = mulHeight.{u_1, u_2} (K := K) (ι := ι) 0
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
ι' : 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
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
have inr : ∀ (hx : x ≠ 0), mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
have inr : ∀ (i : ι) (hi : x i ≠ 0 i), mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
Tactic: obtain ⟨i, hi⟩ := 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_2
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
have this : Nonempty ι
Tactic: have : Nonempty ι := .intro 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
ι' : Type u_3
inst_2 : Finite ι
inst_3 : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
have hx' : 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⟩
-- 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
⊢ mulHeight (ι := ι ⊕ ι') (Sum.elim x 0) = mulHeight x
have 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))
Tactic: rw [mulHeight_eq hx, mulHeight_eq 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
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))
have refine : LE.le (α := ℝ) (⨆ (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
-- 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 ℝ
⊢ LE.le (α := ℝ) (⨆ (j : ι ⊕ ι'), (v : (a : K) → ℝ) (Sum.elim x 0 j)) (⨆ (i : ι), (v : (a : K) → ℝ) (x i))
have refine : ∀ (j : ι ⊕ ι'), LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 j) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
Tactic: refine ciSup_le fun j ↦ ?_
-- 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 : ι ⊕ ι'
⊢ LE.le (α := ℝ) ((v : (a : K) → ℝ) (Sum.elim x 0 j) : ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i) : ℝ)
have 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) : ℝ)
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