awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C₁ : ℝ
hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]
⊢ ∃ (C : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 → |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ C
have obtain : ∀ (C₂ : ℝ)
  (hC₂ :
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 → C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]),
  ∃ (C : ℝ),
    ∀ {a b c d : K},
      ![a, b] ≠ 0 →
        ![c, d] ≠ 0 → |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ C
Tactic: obtain ⟨C₂, hC₂⟩ := logHeight_sym2_ge K
-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (hypothesis)
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C₁ : ℝ
hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]
C₂ : ℝ
hC₂ :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ max C₁ (-C₂)
have hC₃ : C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
Tactic: specialize hC₂ hab hcd
Cleared hypotheses: hC₂
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (AbsoluteValue K ℝ)
v : InfinitePlace K
⊢ Multiset.count (↑v : AbsoluteValue K ℝ) (multisetInfinitePlace K) = v.mult
have have : ∀ (this : DecidableEq (InfinitePlace K)), Multiset.count (↑v : AbsoluteValue K ℝ) (multisetInfinitePlace K) = v.mult
Tactic: have : DecidableEq (InfinitePlace K) := Subtype.instDecidableEq
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f (multisetInfinitePlace K)).prod = ∏ v : InfinitePlace K, f (↑v : AbsoluteValue K ℝ) ^ v.mult
have rw : Eq.{u_2 + 1} (α := M)
  (∏ m ∈ Multiset.toFinset (multisetInfinitePlace K), f m ^ Multiset.count m (multisetInfinitePlace K))
  (∏ v : InfinitePlace K, f (↑v : AbsoluteValue K ℝ) ^ v.mult)
Tactic: rw [Finset.prod_multiset_map_count]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w
⊢ f w ^ Multiset.count w (multisetInfinitePlace K) =
    f
        (↑((fun (w : AbsoluteValue K ℝ)
                  (hw :
                    Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
                Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯)
              w hw) :
          AbsoluteValue K ℝ) ^
      InfinitePlace.mult.{u_1} (K := K)
        ((fun (w : AbsoluteValue K ℝ)
              (hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
            Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯)
          w hw)
have rw : f w ^ InfinitePlace.mult (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w sorry) =
  f
      (↑((fun (w : AbsoluteValue K ℝ)
                (hw :
                  Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
              Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w sorry)
            w hw) :
        AbsoluteValue K ℝ) ^
    InfinitePlace.mult.{u_1} (K := K)
      ((fun (w : AbsoluteValue K ℝ)
            (hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
          Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w sorry)
        w hw)
Tactic: rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w
rw :
  f w ^ InfinitePlace.mult (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯) =
    f
        (↑((fun (w : AbsoluteValue K ℝ)
                  (hw :
                    Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
                Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯)
              w hw) :
          AbsoluteValue K ℝ) ^
      InfinitePlace.mult.{u_1} (K := K)
        ((fun (w : AbsoluteValue K ℝ)
              (hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
            Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯)
          w hw)
⊢ f w ^ Multiset.count w (multisetInfinitePlace K) =
    f
        (↑((fun (w : AbsoluteValue K ℝ)
                  (hw :
                    Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
                Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯)
              w hw) :
          AbsoluteValue K ℝ) ^
      InfinitePlace.mult.{u_1} (K := K)
        ((fun (w : AbsoluteValue K ℝ)
              (hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K)) w) ↦
            Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯)
          w hw)
have rw₁ : ∃ (φ : K →+* ℂ), place φ = w
Tactic: rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f (multisetInfinitePlace K)).prod = ∏ v : InfinitePlace K, f (↑v : AbsoluteValue K ℝ) ^ v.mult
have rw : Eq.{u_2 + 1} (α := M)
  (∏ m ∈ Multiset.toFinset (multisetInfinitePlace K), f m ^ Multiset.count m (multisetInfinitePlace K))
  (∏ v : InfinitePlace K, f (↑v : AbsoluteValue K ℝ) ^ v.mult)
Tactic: classical
  rw [Finset.prod_multiset_map_count]
  exact Finset.prod_bij' (fun w hw ↦ ⟨w, mem_multisetInfinitePlace.mp <| Multiset.mem_dedup.mp hw⟩)
    (fun v _ ↦ v.val) (fun _ _ ↦ Finset.mem_univ _) (fun v _ ↦ by simp [v.isInfinitePlace])
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) fun w hw ↦ by rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f archAbsVal).sum = ∑ v : InfinitePlace K, v.mult • f (↑v : AbsoluteValue K ℝ)
have rw : Eq.{u_2 + 1} (α := M) (∑ m ∈ toFinset archAbsVal, count m archAbsVal • f m)
  (∑ v : InfinitePlace K, v.mult • f (↑v : AbsoluteValue K ℝ))
Tactic: rw [sum_multiset_map_count]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) w
⊢ count w archAbsVal • f w =
    InfinitePlace.mult.{u_1} (K := K)
        ((fun (x1 : AbsoluteValue K ℝ)
              (x2 : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) x1) ↦
            Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) x1 ⋯)
          w hw) •
      f
        (↑((fun (x1 : AbsoluteValue K ℝ)
                  (x2 : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) x1) ↦
                Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) x1 ⋯)
              w hw) :
          AbsoluteValue K ℝ)
have simp : ∀ (hw_1 : IsInfinitePlace w),
  count w (multisetInfinitePlace K) • f w =
    InfinitePlace.mult (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w sorry) • f w
Tactic: simp only [archAbsVal, mem_toFinset, mem_multisetInfinitePlace] at hw ⊢
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f archAbsVal).sum = ∑ v : InfinitePlace K, v.mult • f (↑v : AbsoluteValue K ℝ)
have rw : Eq.{u_2 + 1} (α := M) (∑ m ∈ toFinset archAbsVal, count m archAbsVal • f m)
  (∑ v : InfinitePlace K, v.mult • f (↑v : AbsoluteValue K ℝ))
Tactic: classical
  rw [sum_multiset_map_count]
  exact sum_bij' (⟨·, mem_multisetInfinitePlace.mp <| mem_dedup.mp ·⟩)
    _ (by simp) (by simp [InfinitePlace.isInfinitePlace, archAbsVal]) (by simp) (fun _ _ ↦ rfl)
    fun w hw ↦ by
      simp only [archAbsVal, mem_toFinset, mem_multisetInfinitePlace] at hw ⊢
      simp [count_multisetInfinitePlace_eq_mult ⟨w, hw⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ v : InfinitePlace K, v.mult
have h : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
  Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
Tactic: convert! sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ v : InfinitePlace K, v.mult
have h₁ : ∀ (x : InfinitePlace K),
  Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x → x.mult = HSMul.hSMul (β := ℕ) x.mult 1
Tactic: convert! sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
  List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h₁ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ i : Fin archAbsVal.toList.length, 1
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
h₁ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ i : Fin archAbsVal.toList.length, 1
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h₂ : List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) = ∑ i : Fin archAbsVal.toList.length, 1
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
h₁ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ i : Fin archAbsVal.toList.length, 1
h₂ : List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) = ∑ i : Fin archAbsVal.toList.length, 1
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h₃ : List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) =
  HSMul.hSMul (β := ℕ) (List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal)) 1
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
h₁ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ i : Fin archAbsVal.toList.length, 1
h₂ : List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) = ∑ i : Fin archAbsVal.toList.length, 1
h₃ :
  List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) =
    HSMul.hSMul (β := ℕ) (List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal)) 1
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h₄ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
  HSMul.hSMul (β := ℕ) (Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal) 1
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
h₁ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ i : Fin archAbsVal.toList.length, 1
h₂ : List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) = ∑ i : Fin archAbsVal.toList.length, 1
h₃ :
  List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) =
    HSMul.hSMul (β := ℕ) (List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal)) 1
h₄ :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    HSMul.hSMul (β := ℕ) (Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal) 1
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h₅ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal * 1
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    List.sum (List.map (fun (x : AbsoluteValue K ℝ) ↦ 1) (Multiset.toList archAbsVal))
h₁ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ i : Fin archAbsVal.toList.length, 1
h₂ : List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) = ∑ i : Fin archAbsVal.toList.length, 1
h₃ :
  List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal) =
    HSMul.hSMul (β := ℕ) (List.length.{u_1} (α := AbsoluteValue K ℝ) (Multiset.toList archAbsVal)) 1
h₄ :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    HSMul.hSMul (β := ℕ) (Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal) 1
h₅ :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal * 1
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal)
have h₆ : Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal
Tactic: rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ totalWeight K = Module.finrank ℚ K
have rw : ∑ v : InfinitePlace K, v.mult = Module.finrank ℚ K
Tactic: rw [totalWeight_eq_sum_mult, InfinitePlace.sum_mult_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : ∑ v : InfinitePlace K, v.mult = Module.finrank ℚ K
⊢ totalWeight K = Module.finrank ℚ K
have rw₁ : Module.finrank ℚ K = Module.finrank ℚ K
Tactic: rw [totalWeight_eq_sum_mult, InfinitePlace.sum_mult_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < totalWeight K
have have : ∀ (this : Inhabited (InfinitePlace K)), 0 < totalWeight K
Tactic: have : Inhabited (InfinitePlace K) := Classical.inhabited_of_nonempty'
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
Tactic: have hv : IsNonarchimedean (v ·) := FinitePlace.add_le v
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
Tactic: have H (n : ℤ) : v n ≤ 1 := IsNonarchimedean.apply_intCast_le_one hv
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have obtain : ∀ (f : ι → ℤ) (hf : Finset.gcd Finset.univ x = ∑ a : ι, x a * f a),
  Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
Tactic: obtain ⟨f, hf⟩ := Finset.gcd_eq_sum_mul .univ x
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
f : ι → ℤ
hf : Finset.gcd Finset.univ x = ∑ a : ι, x a * f a
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have hf₁ : Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (↑(Finset.gcd Finset.univ x) : ℚ) : ℝ)
  ((v : (a : ℚ) → ℝ) (↑(∑ a : ι, x a * f a) : ℚ) : ℝ)
Tactic: apply_fun v at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
f : ι → ℤ
hf :
  Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (↑(Finset.gcd Finset.univ x) : ℚ) : ℝ)
    ((v : (a : ℚ) → ℝ) (↑(∑ a : ι, x a * f a) : ℚ) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have hf₁ : Eq (α := ℝ) (1 : ℝ) ((v : (a : ℚ) → ℝ) (∑ x_1 : ι, HMul.hMul (α := ℚ) (↑(x x_1) : ℚ) (↑(f x_1) : ℚ)) : ℝ)
Tactic: simp_rw [hx, Int.cast_one, map_one, Int.cast_sum, Int.cast_mul] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
f : ι → ℤ
hf : Eq (α := ℝ) (1 : ℝ) ((v : (a : ℚ) → ℝ) (∑ x_1 : ι, HMul.hMul (α := ℚ) (↑(x x_1) : ℚ) (↑(f x_1) : ℚ)) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have hf₁ : LE.le (α := ℝ) 1 (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)))
Tactic: replace hf := hf.trans_le hv.apply_sum_univ_le
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
f : ι → ℤ
hf : LE.le (α := ℝ) 1 (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)))
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have obtain : ∀ (i : ι)
  (hi :
    Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
      (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)),
  Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
Tactic: obtain ⟨i, hi⟩ := exists_eq_ciSup_of_finite (f := fun i ↦ v (x i * f i))
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
f : ι → ℤ
hf : LE.le (α := ℝ) 1 (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)))
i : ι
hi :
  Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
    (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have hf₁ : 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ) ((v : (a : ℚ) → ℝ) (↑(f i) : ℚ) : ℝ)
Tactic: rw [← hi, map_mul] at hf
Cleared hypotheses: hf, hi
-- Lean 4 proof step from Mathlib.NumberTheory.Height.NumberField (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
hv : IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x
H : ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
f : ι → ℤ
i : ι
hf : 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ) ((v : (a : ℚ) → ℝ) (↑(f i) : ℚ) : ℝ)
hi :
  Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
    (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
have hf₁ : LE.le (α := ℝ) (1 : ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ)
Tactic: replace hf : 1 ≤ v (x i) := hf.trans <| mul_le_of_le_one_right (apply_nonneg v _) (H _)
Cleared hypotheses: hf