awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K}
    (_h :
      ∀ (k : Fin 4),
        ∑ j : Fin 3,
            HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial (Fin 4) K) → K) (q (k, j)) : K)
              ((eval x : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
          x k ^ HAdd.hAdd (α := ℕ) 1 1),
    C * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
      (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp [p]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K}
    (_h :
      ∀ (k : Fin 4),
        ∑ j : Fin 3,
            HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial (Fin 4) K) → K) (q (k, j)) : K)
              ((eval x : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
          x k ^ HAdd.hAdd (α := ℕ) 1 1),
    C * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
      (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp [p]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, HAdd.hAdd (α := MvPolynomial (Fin 4) K) (X 1) (X 2), X 3]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K}
    (_h :
      ∀ (k : Fin 4),
        ∑ j : Fin 3,
            HMul.hMul (α := K) (β := K) ((eval x : (a : MvPolynomial (Fin 4) K) → K) (q (k, j)) : K)
              ((eval x : (a : MvPolynomial (Fin 4) K) → K) (p j) : K) =
          x k ^ HAdd.hAdd (α := ℕ) 1 1),
    C * mulHeight x ≤ mulHeight.{u_4, 0} (K := K) fun (j : Fin 3) ↦ (eval x : (a : MvPolynomial (Fin 4) K) → K) (p j)
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a * c, a * d + b * c, b * d] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    (eval ![a * c, a * d, b * c, b * d] : (a : MvPolynomial (Fin 4) K) → K)
      (p ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp [p]
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
obtain :
  ∀ (C' : ℝ) (hC₀ : C' > 0)
    (hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]),
    ∃ (C : ℝ), ∀ (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), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]

Tactic:
obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_le K

Premises used: Height.mulHeight_sym2_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
⊢ ∃ (C : ℝ), ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]

Tactic:
⟨log C', fun a b c d ↦ ?_⟩

Premises used: Real.log, Exists.intro
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
refine : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ log C' + logHeight ![a, b] + logHeight ![c, d]
⊢ ∃ (C : ℝ), ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]

Tactic:
refine ⟨log C', fun a b c d ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
a b c d : K
pull : log (mulHeight ![a * c, a * d + b * c, b * d]) ≤ log (C' * mulHeight ![a, b] * mulHeight ![c, d])
⊢ log (mulHeight ![a * c, a * d + b * c, b * d]) ≤ log C' + log (mulHeight ![a, b]) + log (mulHeight ![c, d])

Tactic:
pull (disch := positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
a b c d : K
⊢ 0 < mulHeight ![a * c, a * d + b * c, b * d]

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
a b c d : K
⊢ log (mulHeight ![a * c, a * d + b * c, b * d]) ≤ log (C' * mulHeight ![a, b] * mulHeight ![c, d])

Tactic:
exact log_le_log (by positivity) (hC ..)

Premises used: Real.log_le_log
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
obtain :
  ∀ (C' : ℝ) (hC₀ : C' > 0)
    (hC :
      ∀ {a b c d : K},
        ![a, b] ≠ 0 →
          ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]),
    ∃ (C : ℝ),
      ∀ {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 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

Tactic:
obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_ge K

Premises used: Height.mulHeight_sym2_ge
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
⊢ ∃ (C : ℝ),
    ∀ {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]

Tactic:
⟨log C', fun hab hcd ↦ ?_⟩

Premises used: Real.log, Exists.intro
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
refine :
  ∀ {a b c d : K} (hab : ![a, b] ≠ 0) (hcd : ![c, d] ≠ 0),
    log 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 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

Tactic:
refine ⟨log C', fun hab hcd ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
pull : log (C' * mulHeight ![a, b] * mulHeight ![c, d]) ≤ log (mulHeight ![a * c, a * d + b * c, b * d])
⊢ log C' + log (mulHeight ![a, b]) + log (mulHeight ![c, d]) ≤ log (mulHeight ![a * c, a * d + b * c, b * d])

Tactic:
pull (disch := positivity) log

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ 0 < C' * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ log (C' * mulHeight ![a, b] * mulHeight ![c, d]) ≤ log (mulHeight ![a * c, a * d + b * c, b * d])

Tactic:
exact log_le_log (by positivity) (hC hab hcd)

Premises used: Real.log_le_log
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
obtain :
  ∀ (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
⊢ ∃ (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_le K

Premises used: Height.logHeight_sym2_le
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]
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
⊢ ∃ (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

Premises used: Height.logHeight_sym2_ge
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
⊢ C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

Tactic:
specialize hC₂ hab hcd
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
hC₂ : C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
⊢ |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ max C₁ (-C₂)

Tactic:
grind
-- Module: Mathlib.NumberTheory.Height.MvPolynomial
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]
⊢ ∃ (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:
exact ⟨max C₁ (-C₂), fun hab hcd ↦ by specialize hC₂ hab hcd; grind⟩
-- Module: Mathlib.NumberTheory.Height.Northcott
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
inst_2 : Northcott.{u_1, 0} (α := K) mulHeight₁
⊢ Northcott.{u_1, 0} (α := K) logHeight₁

Tactic:
comp_of_bddAbove mulHeight₁ log fun B ↦ bddAbove_def.mpr ⟨exp B, fun _ ↦ le_exp_of_log_le⟩

Premises used: Iff.mpr, Northcott.comp_of_bddAbove, Height.logHeight₁, Real.exp, Real.log, dite, Exists.intro, Height.mulHeight₁, Real.le_exp_of_log_le, bddAbove_def
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : AbsoluteValue K ℝ
⊢ Membership.mem (γ := Multiset (AbsoluteValue K ℝ)) (multisetInfinitePlace K) v ↔ IsInfinitePlace v

Tactic:
simp [multisetInfinitePlace, Multiset.mem_replicate, isInfinitePlace_iff, eq_comm (a := v)]

Premises used: NumberField.isInfinitePlace_iff, NumberField.multisetInfinitePlace, eq_comm, Multiset.mem_replicate
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (AbsoluteValue K ℝ)
v : InfinitePlace K
have :
  ∀ (this : DecidableEq (InfinitePlace K)), Multiset.count (↑v : AbsoluteValue K ℝ) (multisetInfinitePlace K) = v.mult
⊢ Multiset.count (↑v : AbsoluteValue K ℝ) (multisetInfinitePlace K) = v.mult

Tactic:
have : DecidableEq (InfinitePlace K) := Subtype.instDecidableEq
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (AbsoluteValue K ℝ)
v : InfinitePlace K
this : DecidableEq (InfinitePlace K)
⊢ Multiset.count (↑v : AbsoluteValue K ℝ) (multisetInfinitePlace K) = v.mult

Tactic:
simpa only [multisetInfinitePlace, Multiset.count_bind, Finset.sum_map_val,
    Multiset.count_replicate, ← Subtype.ext_iff] using Fintype.sum_ite_eq' v ..

Premises used: Fintype.sum_ite_eq', Multiset.count_replicate, NumberField.multisetInfinitePlace, Subtype.ext_iff, Multiset.count_bind, Finset.sum_map_val
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
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)
⊢ (Multiset.map f (multisetInfinitePlace K)).prod = ∏ v : InfinitePlace K, f (↑v : AbsoluteValue K ℝ) ^ v.mult

Tactic:
rw [Finset.prod_multiset_map_count]

Premises used: Finset.prod_multiset_map_count
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
v : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ v
⊢ Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (Multiset.toFinset (multisetInfinitePlace K))
    ((fun (v : InfinitePlace K) (x : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ v) ↦
        (↑v : AbsoluteValue K ℝ))
      v h)

Tactic:
simp [v.isInfinitePlace]

Premises used: NumberField.InfinitePlace.isInfinitePlace
-- Module: Mathlib.NumberTheory.Height.NumberField
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)
rw₁ : ∃ (φ : K →+* ℂ), place φ = 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)
rw₃ : ∃ (φ : K →+* ℂ), place φ = 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)

Tactic:
rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]

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 : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ 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:
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, _⟩]

Premises used: Finset.mem_univ, Finset.prod_bij'
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid M
f : AbsoluteValue K ℝ → M
rw rw₁ 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)
⊢ (Multiset.map f (multisetInfinitePlace K)).prod = ∏ 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, _⟩]

Premises used: Finset.mem_univ, Finset.prod_multiset_map_count, Finset.prod_bij'
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
v : AbsoluteValue K ℝ
hv : Membership.mem (γ := Set (AbsoluteValue K ℝ)) {v : AbsoluteValue K ℝ | IsFinitePlace v} v
⊢ ∃ (v_1 : IsDedekindDomain.HeightOneSpectrum (𝓞 K)),
    place (A := IsDedekindDomain.HeightOneSpectrum.adicCompletion K v_1) (FinitePlace.embedding v_1) = v

Tactic:
simpa using hv
-- Module: Mathlib.NumberTheory.Height.NumberField
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 archAbsVal).prod = ∏ v : InfinitePlace K, f (↑v : AbsoluteValue K ℝ) ^ v.mult

Tactic:
prod_multisetInfinitePlace_eq f

Premises used: _private.0.NumberField.prod_multisetInfinitePlace_eq
-- Module: Mathlib.NumberTheory.Height.NumberField
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
M : Type u_2
inst_2 : CommMonoid 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
M : Type u_2
inst_2 : AddCommMonoid M
f : AbsoluteValue K ℝ → M
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:
rw [sum_multiset_map_count]

Premises used: Finset.sum_multiset_map_count
-- 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
⊢ ∀ (a : AbsoluteValue K ℝ) (ha : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) a),
    Membership.mem (γ := Finset (InfinitePlace K)) univ
      ((fun (x1 : AbsoluteValue K ℝ) (x2 : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) x1) ↦
          Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) x1 ⋯)
        a ha)

Tactic:
simp
-- 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
⊢ ∀ (a : InfinitePlace K) (ha : Membership.mem (γ := Finset (InfinitePlace K)) univ a),
    Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) (↑a : AbsoluteValue K ℝ)

Tactic:
simp [InfinitePlace.isInfinitePlace, archAbsVal]

Premises used: NumberField.InfinitePlace.isInfinitePlace, Height.AdmissibleAbsValues.archAbsVal
-- 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
⊢ ∀ (a : AbsoluteValue K ℝ) (ha : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) a),
    (↑((fun (x1 : AbsoluteValue K ℝ) (x2 : Membership.mem (γ := Finset (AbsoluteValue K ℝ)) (toFinset archAbsVal) x1) ↦
              Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) x1 ⋯)
            a ha) :
        AbsoluteValue K ℝ) =
      a

Tactic:
simp