awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodySum K B)
w : K
h_mem : Membership.mem (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K) w
h_nz : w ≠ 0
h_bd : (↑|(Algebra.norm ℚ : (a : K) → ℚ) w| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
⊢ ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
have obtain : ∀ (a : 𝓞 K)
  (h_mem :
    Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K))
  (h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K))
  (h_bd :
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
      (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K),
  ∃ (a : 𝓞 K), a ≠ 0 ∧ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤ (B / (↑(finrank ℚ K) : ℝ)) ^ finrank ℚ K
Tactic: obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
Cleared hypotheses: w, h_mem, h_nz, h_bd
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
x x_1 : (𝓞 K)ˣ
x_2 : mixedSpace K
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have simp_rw : HMul.hMul (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x * x_1) : 𝓞 K)) :
      mixedSpace K)
    x_2 =
  HMul.hMul (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
    (HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
      x_2)
Tactic: simp_rw [unitSMul_smul, Units.coe_mul, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
x x_1 : (𝓞 K)ˣ
x_2 : mixedSpace K
simp_rw :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x * x_1) : 𝓞 K)) :
        mixedSpace K)
      x_2 =
    HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
        x_2)
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have simp_rw₁ : HMul.hMul (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K) : K)) :
      mixedSpace K)
    x_2 =
  HMul.hMul (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
    (HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
      x_2)
Tactic: simp_rw [unitSMul_smul, Units.coe_mul, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
x x_1 : (𝓞 K)ˣ
x_2 : mixedSpace K
simp_rw :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x * x_1) : 𝓞 K)) :
        mixedSpace K)
      x_2 =
    HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
        x_2)
simp_rw₁ :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K) : K)) :
        mixedSpace K)
      x_2 =
    HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
        x_2)
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have simp_rw₂ : HMul.hMul (α := mixedSpace K) (β := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K) *
    x_2 =
  HMul.hMul (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) : mixedSpace K)
    (HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x_1 : 𝓞 K)) : mixedSpace K)
      x_2)
Tactic: simp_rw [unitSMul_smul, Units.coe_mul, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ HSMul.hSMul (α := (𝓞 K)ˣ) 1 x = x
have simp_rw : HMul.hMul (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K)) : mixedSpace K) x =
  x
Tactic: simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
simp_rw :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K)) : mixedSpace K) x =
    x
⊢ HSMul.hSMul (α := (𝓞 K)ˣ) 1 x = x
have simp_rw₁ : (mixedEmbedding K : (a : K) → mixedSpace K) 1 * x = x
Tactic: simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
simp_rw :
  HMul.hMul (α := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K)) : mixedSpace K) x =
    x
simp_rw₁ : (mixedEmbedding K : (a : K) → mixedSpace K) 1 * x = x
⊢ HSMul.hSMul (α := (𝓞 K)ˣ) 1 x = x
have simp_rw₂ : 1 * x = x
Tactic: simp_rw [unitSMul_smul, Units.coe_one, map_one, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ u • x = 0
have rw : HSMul.hSMul (β := mixedSpace K) u 0 = 0
Tactic: rw [h, smul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
rw : HSMul.hSMul (β := mixedSpace K) u 0 = 0
⊢ u • x = 0
have rw₁ : Eq.{u_1 + 1} (α := mixedSpace K) 0 0
Tactic: rw [h, smul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ u • x = 0 ↔ x = 0
have refine : ∀ (h : u • x = 0), x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, smul_zero]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : u • x = 0
⊢ x = 0
have contrapose! : ∀ (h : x ≠ 0), u • x ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x ≠ 0
⊢ u • x ≠ 0
have obtain : ∀ (w : InfinitePlace K) (h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)), u • x ≠ 0
Tactic: obtain ⟨w, h⟩ := exists_normAtPlace_ne_zero_iff.mpr h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ u • x ≠ 0
have refine : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (u • x) : ℝ) (0 : ℝ)
Tactic: refine exists_normAtPlace_ne_zero_iff.mp ⟨w, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h_1 : x ≠ 0
w : InfinitePlace K
h : Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (u • x) : ℝ) (0 : ℝ)
have rw : HMul.hMul (α := ℝ) (β := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) ≠
  0
Tactic: rw [unitSMul_smul, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) : mixedSpace K) =
      (mixedEmbedding K : (a : K) → mixedSpace K) (↑y : K) ↔
    (↑u : 𝓞 K) * x = y
have I : Function.Injective (α := K) (β := mixedSpace K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)
Tactic: rw [unitSMul_smul, ← map_mul, Function.Injective.eq_iff, ← RingOfIntegers.coe_eq_algebraMap,
    ← map_mul, ← RingOfIntegers.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (u • x) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have rw : Eq (α := ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
        x) :
    ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: rw [unitSMul_smul, map_mul, norm_unit, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        (HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
          x) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (u • x) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have rw₁ : HMul.hMul (α := ℝ) (β := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
Tactic: rw [unitSMul_smul, map_mul, norm_unit, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        (HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
          x) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
rw₁ :
  HMul.hMul (α := ℝ) (β := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) :
            mixedSpace K) :
        ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
    (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (u • x) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have rw₂ : HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
Tactic: rw [unitSMul_smul, map_mul, norm_unit, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
rw :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        (HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
          x) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
rw₁ :
  HMul.hMul (α := ℝ) (β := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) :
            mixedSpace K) :
        ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
    (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
rw₂ :
  HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) =
    (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (u • x) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have rw₃ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
Tactic: rw [unitSMul_smul, map_mul, norm_unit, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq.{u_1 + 1} (α := logSpace K) (logMap 0) 0
have h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }), logMap 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq.{u_1 + 1} (α := logSpace K) (logMap 1) 0
have h : ∀ (x : { w : InfinitePlace K // w ≠ w₀ }), logMap 1 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
⊢ logMap (x * y) = HAdd.hAdd (α := logSpace K) (logMap x) (logMap y)
have h : ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
  logMap (x * y) w = HAdd.hAdd (α := logSpace K) (β := logSpace K) (logMap x) (logMap y) w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) (x * y)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (x * y)) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
have h : (↑(↑w : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) +
        Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
      (Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹ +
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)) =
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
Tactic: rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) +
          Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        (Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹ +
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)) =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
⊢ (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) (x * y)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (x * y)) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
have h₁ : Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
hx : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
hy : Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) +
          Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
        (Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹ +
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)) =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
h₁ : Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) (x * y)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (x * y)) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y) -
          Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) y) * (↑(finrank ℚ K) : ℝ)⁻¹)
have h₂ : Ne (α := ℝ) ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) y : ℝ) (0 : ℝ)
Tactic: rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
have rw : (↑(↑w : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
      Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
Tactic: rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
rw :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
⊢ logMap x w =
    (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
have rw₁ : (↑(↑w : InfinitePlace K).mult : ℝ) *
    (Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) - Real.log 1 * (↑(finrank ℚ K) : ℝ)⁻¹) =
  (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log ((normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x)
Tactic: rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]