awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.NumberField
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
simp :
  ∀ (hw_1 : IsInfinitePlace w),
    count w (multisetInfinitePlace K) • f w =
      InfinitePlace.mult (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯) • f 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 ℝ)

Tactic:
simp only [archAbsVal, mem_toFinset, mem_multisetInfinitePlace] at hw ⊢

Premises used: Height.AdmissibleAbsValues.archAbsVal, NumberField.mem_multisetInfinitePlace, Multiset.mem_toFinset
-- Module: Mathlib.NumberTheory.Height.NumberField
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_1 : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) w
hw : IsInfinitePlace w
⊢ count w (multisetInfinitePlace K) • f w =
    InfinitePlace.mult (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) w ⋯) • f w

Tactic:
simp [count_multisetInfinitePlace_eq_mult ⟨w, hw⟩]

Premises used: Subtype.mk, NumberField.count_multisetInfinitePlace_eq_mult
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ Eq.{u_2 + 1} (α := M) (∑ m ∈ toFinset archAbsVal, count m archAbsVal • f m)
    (∑ v : InfinitePlace K, v.mult • f (↑v : AbsoluteValue K ℝ))

Tactic:
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⟩]

Premises used: Finset.sum_bij'
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
rw rw₁ rw₂ :
  Eq.{u_2 + 1} (α := M) (∑ m ∈ toFinset archAbsVal, count m archAbsVal • f m)
    (∑ v : InfinitePlace K, v.mult • f (↑v : AbsoluteValue K ℝ))
⊢ (Multiset.map f archAbsVal).sum = ∑ 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⟩]

Premises used: Finset.sum_multiset_map_count, Finset.sum_bij'
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ Eq.{u_2 + 1} (α := M) (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), f (↑v : AbsoluteValue K ℝ))
    (∑ᶠ (v : FinitePlace K), f (↑v : AbsoluteValue K ℝ))

Tactic:
rfl

Premises used: NumberField.IsFinitePlace, Set.Mem, setOf, rfl, NumberField.FinitePlace
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ mulHeight₁ x =
    HMul.hMul (α := ℝ) (∏ v : InfinitePlace K, HPow.hPow (α := ℝ) (max ((v : (a : K) → ℝ) x) 1 : ℝ) v.mult)
      (∏ᶠ (v : FinitePlace K), max ((v : (a : K) → ℝ) x) 1)

Tactic:
simp only [FinitePlace.coe_apply, InfinitePlace.coe_apply, Height.mulHeight₁_eq,
    prod_archAbsVal_eq, prod_nonarchAbsVal_eq fun v ↦ max (v x) 1]

Premises used: NumberField.prod_nonarchAbsVal_eq, Height.mulHeight₁_eq, NumberField.InfinitePlace.coe_apply, NumberField.FinitePlace.coe_apply, Max.max, NumberField.prod_archAbsVal_eq, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ logHeight₁ x =
    HAdd.hAdd (α := ℝ) (∑ v : InfinitePlace K, (↑v.mult : ℝ) * log⁺ ((v : (a : K) → ℝ) x))
      (∑ᶠ (v : FinitePlace K), log⁺ ((v : (a : K) → ℝ) x))

Tactic:
simp only [← nsmul_eq_mul, FinitePlace.coe_apply, InfinitePlace.coe_apply, Height.logHeight₁_eq,
    sum_archAbsVal_eq, sum_nonarchAbsVal_eq fun v ↦ log⁺ (v x)]

Premises used: Real.posLog, NumberField.InfinitePlace.coe_apply, Height.logHeight₁_eq, NumberField.sum_nonarchAbsVal_eq, NumberField.FinitePlace.coe_apply, nsmul_eq_mul, DFunLike.coe, NumberField.sum_archAbsVal_eq
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
x : ι → K
hx : x ≠ 0
⊢ mulHeight x =
    HMul.hMul (α := ℝ) (∏ v : InfinitePlace K, HPow.hPow (α := ℝ) (⨆ (i : ι), (v : (a : K) → ℝ) (x i)) v.mult)
      (∏ᶠ (v : FinitePlace K), ⨆ (i : ι), (v : (a : K) → ℝ) (x i))

Tactic:
simp only [FinitePlace.coe_apply, InfinitePlace.coe_apply, Height.mulHeight_eq hx,
    prod_archAbsVal_eq, prod_nonarchAbsVal_eq fun v ↦ ⨆ i, v (x i)]

Premises used: NumberField.prod_nonarchAbsVal_eq, NumberField.InfinitePlace.coe_apply, iSup, Height.mulHeight_eq, NumberField.FinitePlace.coe_apply, NumberField.prod_archAbsVal_eq, DFunLike.coe
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℕ) (Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) archAbsVal))
    (∑ v : InfinitePlace K, HSMul.hSMul (β := ℕ) v.mult 1)

Tactic:
sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))

Premises used: OfNat.ofNat, NumberField.sum_archAbsVal_eq
-- Module: Mathlib.NumberTheory.Height.NumberField
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)
h₁ :
  ∀ (x : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x → x.mult = HSMul.hSMul (β := ℕ) x.mult 1
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = ∑ v : InfinitePlace K, v.mult

Tactic:
convert! sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))

Premises used: OfNat.ofNat, NumberField.sum_archAbsVal_eq
-- Module: Mathlib.NumberTheory.Height.NumberField
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
h₆ h₇ :
  Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal = Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal
⊢ Multiset.card.{u_1} (α := AbsoluteValue K ℝ) archAbsVal =
    Multiset.sum (Multiset.map (fun (x : AbsoluteValue K ℝ) ↦ 1) 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]

Premises used: Multiset.length_toList, smul_eq_mul, mul_one, Fin.sum_const, Fin.sum_univ_fun_getElem, Multiset.sum_map_toList
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
⊢ x.mult = HSMul.hSMul (β := ℕ) x.mult 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : ∑ v : InfinitePlace K, v.mult = Module.finrank ℚ K
rw₁ rw₂ : Module.finrank ℚ K = Module.finrank ℚ K
⊢ totalWeight K = Module.finrank ℚ K

Tactic:
rw [totalWeight_eq_sum_mult, InfinitePlace.sum_mult_eq]

Premises used: NumberField.InfinitePlace.sum_mult_eq, NumberField.totalWeight_eq_sum_mult
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
have : ∀ (this : Inhabited (InfinitePlace K)), 0 < totalWeight K
⊢ 0 < totalWeight K

Tactic:
have : Inhabited (InfinitePlace K) := Classical.inhabited_of_nonempty'
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : Inhabited (InfinitePlace K)
⊢ 0 < totalWeight K

Tactic:
simpa [totalWeight, archAbsVal, multisetInfinitePlace]
    using Fintype.sum_pos
      (Function.ne_iff.mpr ⟨default, (default : InfinitePlace K).mult_ne_zero⟩).pos

Premises used: Fintype.sum_pos, NumberField.multisetInfinitePlace, Height.AdmissibleAbsValues.archAbsVal, Height.totalWeight
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.gcd Finset.univ x = 1
⊢ IsNonarchimedean (R := ℝ) fun (x : ℚ) ↦ (v : (a : ℚ) → ℝ) x

Tactic:
have hv : IsNonarchimedean (v ·) := FinitePlace.add_le v
-- Module: Mathlib.NumberTheory.Height.NumberField
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
⊢ ∀ (n : ℤ), LE.le (α := ℝ) ((v : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)

Tactic:
have H (n : ℤ) : v n ≤ 1 := IsNonarchimedean.apply_intCast_le_one hv
-- Module: Mathlib.NumberTheory.Height.NumberField
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 : ℝ)
obtain :
  ∀ (f : ι → ℤ) (hf : Finset.gcd Finset.univ x = ∑ a : ι, x a * f a),
    Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1

Tactic:
obtain ⟨f, hf⟩ := Finset.gcd_eq_sum_mul .univ x

Premises used: Finset.univ, Finset.gcd_eq_sum_mul
-- Module: Mathlib.NumberTheory.Height.NumberField
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 (α := ℝ) ((v : (a : ℚ) → ℝ) (↑(Finset.gcd Finset.univ x) : ℚ) : ℝ)
    ((v : (a : ℚ) → ℝ) (↑(∑ a : ι, x a * f a) : ℚ) : ℝ)

Tactic:
apply_fun v at hf
-- Module: Mathlib.NumberTheory.Height.NumberField
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 (α := ℝ) (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

Premises used: Int.cast_sum, Int.cast_mul, map_one, Int.cast_one
-- Module: Mathlib.NumberTheory.Height.NumberField
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) : ℚ)) : ℝ)
⊢ LE.le (α := ℝ) 1 (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)))

Tactic:
replace hf := hf.trans_le hv.apply_sum_univ_le
-- Module: Mathlib.NumberTheory.Height.NumberField
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) : ℚ)))
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
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1

Tactic:
obtain ⟨i, hi⟩ := exists_eq_ciSup_of_finite (f := fun i ↦ v (x i * f i))

Premises used: exists_eq_ciSup_of_finite
-- Module: Mathlib.NumberTheory.Height.NumberField
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) : ℚ)) : ℝ)
⊢ 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ) ((v : (a : ℚ) → ℝ) (↑(f i) : ℚ) : ℝ)

Tactic:
rw [← hi, map_mul] at hf

Premises used: map_mul
-- Module: Mathlib.NumberTheory.Height.NumberField
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) : ℚ)) : ℝ)
hf₁ : 1 ≤ HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ) ((v : (a : ℚ) → ℝ) (↑(f i) : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
    (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)

Tactic:
rw [← hi, map_mul] at hf

Premises used: map_mul
-- Module: Mathlib.NumberTheory.Height.NumberField
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) : ℚ)) : ℝ)
⊢ 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 _)
-- Module: Mathlib.NumberTheory.Height.NumberField
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 : ι
hi :
  Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
    (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
hf : LE.le (α := ℝ) (1 : ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1

Tactic:
le_antisymm (ciSup_le (H <| x ·)) <| Finite.le_ciSup_of_le i hf

Premises used: le_antisymm, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.NumberField
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 : ι
hi :
  Eq (α := ℝ) ((v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
    (⨆ (i : ι), (v : (a : ℚ) → ℝ) (HMul.hMul (α := ℚ) (↑(x i) : ℚ) (↑(f i) : ℚ)) : ℝ)
hf : LE.le (α := ℝ) (1 : ℝ) ((v : (a : ℚ) → ℝ) (↑(x i) : ℚ) : ℝ)
⊢ Eq (α := ℝ) (⨆ (i : ι), (v : (a : ℚ) → ℝ) (↑(x i) : ℚ)) 1

Tactic:
exact le_antisymm (ciSup_le (H <| x ·)) <| Finite.le_ciSup_of_le i hf

Premises used: le_antisymm, Finite.le_ciSup_of_le, ciSup_le
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
contrapose! : ∀ (hx : Eq (α := ι → ℚ) (Int.cast ∘ x) 0), Finset.gcd Finset.univ x ≠ 1
⊢ Ne (α := ι → ℚ) (Int.cast ∘ x) 0

Tactic:
contrapose! hx
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Eq (α := ι → ℚ) (Int.cast ∘ x) 0
⊢ x = 0

Tactic:
rw [Function.comp_eq_zero_iff x intCast_injective Rat.intCast_zero] at hx

Premises used: Function.comp_eq_zero_iff, Rat.intCast_zero, Rat.intCast_injective
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → Eq (α := ℤ) (0 x) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : x = 0
rw : Ne (α := ℤ) 0 1
⊢ Finset.gcd Finset.univ x ≠ 1

Tactic:
rw [hx, Finset.gcd_eq_zero_iff.mpr (by simp)]

Premises used: Iff.mpr, Finset.gcd_eq_zero_iff
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ Ne (α := ℤ) 0 1

Tactic:
zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ Ne (α := ℤ) 0 1

Tactic:
exact zero_ne_one

Premises used: zero_ne_one
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
⊢ Ne (α := ι → ℚ) (Int.cast ∘ x) 0

Tactic:
have hx₀ : Int.cast ∘ x ≠ (0 : ι → ℚ) := by
    contrapose! hx
    rw [Function.comp_eq_zero_iff x intCast_injective Rat.intCast_zero] at hx
    rw [hx, Finset.gcd_eq_zero_iff.mpr (by simp)]
    exact zero_ne_one
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
hx₀ : Ne (α := ι → ℚ) (Int.cast ∘ x) 0
simp_rw :
  HMul.hMul (α := ℝ) (∏ x_1 : InfinitePlace ℚ, HPow.hPow (α := ℝ) (⨆ (i : ι), (↑|(Int.cast ∘ x) i| : ℝ)) x_1.mult)
      (∏ᶠ (v : FinitePlace ℚ), ⨆ (i : ι), (v : (a : ℚ) → ℝ) ((Int.cast ∘ x) i)) =
    ⨆ (i : ι), (↑|x i| : ℝ)
⊢ mulHeight (K := ℚ) (Int.cast ∘ x) = (↑(⨆ (i : ι), |x i|) : ℝ)

Tactic:
simp_rw [Finite.map_iSup_of_monotone _ Int.cast_mono, NumberField.mulHeight_eq hx₀,
    infinitePlace_apply]

Premises used: NumberField.mulHeight_eq, Int.cast_mono, Rat.infinitePlace_apply, Finite.map_iSup_of_monotone
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
hx₀ : Ne (α := ι → ℚ) (Int.cast ∘ x) 0
⊢ HMul.hMul (α := ℝ) (∏ x_1 : InfinitePlace ℚ, HPow.hPow (α := ℝ) (⨆ (i : ι), (↑|(Int.cast ∘ x) i| : ℝ)) x_1.mult)
      (∏ᶠ (v : FinitePlace ℚ), ⨆ (i : ι), (v : (a : ℚ) → ℝ) ((Int.cast ∘ x) i)) =
    ⨆ (i : ι), (↑|x i| : ℝ)

Tactic:
simp [finprod_eq_one_of_forall_eq_one (iSup_finitePlace_apply_eq_one_of_gcd_eq_one · hx)]

Premises used: finprod_eq_one_of_forall_eq_one, Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_one
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
x : ι → ℤ
hx : Finset.gcd Finset.univ x = 1
rw : log (mulHeight (K := ℚ) (Int.cast ∘ x)) = log (↑(⨆ (i : ι), |x i|) : ℝ)
rw₁ rw₂ : log (↑(⨆ (i : ι), |x i|) : ℝ) = log (↑(⨆ (i : ι), |x i|) : ℝ)
⊢ logHeight (K := ℚ) (Int.cast ∘ x) = log (↑(⨆ (i : ι), |x i|) : ℝ)

Tactic:
rw [logHeight_eq_log_mulHeight, mulHeight_eq_max_abs_of_gcd_eq_one hx]

Premises used: Rat.mulHeight_eq_max_abs_of_gcd_eq_one, Height.logHeight_eq_log_mulHeight
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
⊢ Ne (α := ℚ) (↑q.den : ℚ) 0

Tactic:
have hq₀ : (q.den : ℚ) ≠ 0 := mod_cast q.den_nz
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
hq₀ : Ne (α := ℚ) (↑q.den : ℚ) 0
rw : mulHeight (HSMul.hSMul (α := ℚ) (↑q.den : ℚ) ![q, 1]) = mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑q.den : ℚ)]
⊢ mulHeight ![q, 1] = mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑q.den : ℚ)]

Tactic:
rw [← mulHeight_smul_eq_mulHeight _ hq₀]

Premises used: Height.mulHeight_smul_eq_mulHeight
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
hq₀ : Ne (α := ℚ) (↑q.den : ℚ) 0
⊢ mulHeight (HSMul.hSMul (α := ℚ) (↑q.den : ℚ) ![q, 1]) = mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑q.den : ℚ)]

Tactic:
simp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
rw : mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] = (↑(max q.num.natAbs q.den) : ℝ)
⊢ mulHeight₁ q = (↑(max q.num.natAbs q.den) : ℝ)

Tactic:
rw [mulHeight₁_eq_mulHeight, mulHeight_self_one_eq_mulHeight_num_den, ← intCast_natCast q.den]

Premises used: Rat.den, Height.mulHeight₁_eq_mulHeight, Rat.mulHeight_self_one_eq_mulHeight_num_den, Rat.intCast_natCast
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
⊢ Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1

Tactic:
simpa [Finset.univ_fin2, Int.normalize_coe_nat, ← Int.coe_gcd q.num q.den] using
      Int.isCoprime_iff_gcd_eq_one.mp <| isCoprime_num_den q

Premises used: Rat.num, Int.isCoprime_iff_gcd_eq_one, Rat.isCoprime_num_den, Rat.den, Int.normalize_coe_nat, Finset.univ_fin2, Nat.cast, Int.coe_gcd, Iff.mp
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
⊢ Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1

Tactic:
have : (.univ : Finset (Fin 2)).gcd ![q.num, q.den] = 1 := by
    simpa [Finset.univ_fin2, Int.normalize_coe_nat, ← Int.coe_gcd q.num q.den] using
      Int.isCoprime_iff_gcd_eq_one.mp <| isCoprime_num_den q
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
⊢ mulHeight (K := ℚ) (Int.cast ∘ ![q.num, (↑q.den : ℤ)]) = (↑(⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|) : ℝ)

Tactic:
mulHeight_eq_max_abs_of_gcd_eq_one this

Premises used: Rat.mulHeight_eq_max_abs_of_gcd_eq_one
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
q : ℚ
this : Finset.gcd Finset.univ ![q.num, (↑q.den : ℤ)] = 1
h : Eq (α := Fin (Nat.succ 0).succ → ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] (Int.cast ∘ ![q.num, (↑q.den : ℤ)])
h₁ : Eq (α := ℝ) (↑(max q.num.natAbs q.den) : ℝ) (↑(⨆ (i : Fin 2), |![q.num, (↑q.den : ℤ)] i|) : ℝ)
⊢ mulHeight (K := ℚ) ![(↑q.num : ℚ), (↑(↑q.den : ℤ) : ℚ)] = (↑(max q.num.natAbs q.den) : ℝ)

Tactic:
convert! mulHeight_eq_max_abs_of_gcd_eq_one this

Premises used: Rat.mulHeight_eq_max_abs_of_gcd_eq_one