awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₅ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₇ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₈ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₉ : (↑(↑x : InfinitePlace K).mult : ℝ) *
    (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
  0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₉ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₁₀ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * 1) = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₉ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁₀ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * 1) = 0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₁₁ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c|) = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₉ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁₀ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * 1) = 0 x
h₁₁ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c|) = 0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₁₂ : HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) 0 = 0 x
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₉ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁₀ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * 1) = 0 x
h₁₁ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c|) = 0 x
h₁₂ : HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) 0 = 0 x
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₁₃ : Eq (α := ℝ) 0 (0 x)
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (HSMul.hSMul (β := mixedSpace K) c 1)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (HMul.hMul (β := ℝ) |c| ((normAtPlace (↑x : InfinitePlace K) : (a : mixedSpace K) → ℝ) 1 : ℝ)) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) -
        Real.log (HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ)) *
          (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log (|c| * 1) - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₅ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K * 1) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₆ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K) : ℝ)⁻¹) = 0 x
h₇ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - (↑(finrank ℚ K) : ℝ) * Real.log |c| * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₈ :
  (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₉ :
  (↑(↑x : InfinitePlace K).mult : ℝ) *
      (Real.log |c| - Real.log |c| * HMul.hMul (α := ℝ) (↑(finrank ℚ K) : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹) =
    0 x
h₁₀ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c| * 1) = 0 x
h₁₁ : (↑(↑x : InfinitePlace K).mult : ℝ) * (Real.log |c| - Real.log |c|) = 0 x
h₁₂ : HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) 0 = 0 x
h₁₃ : Eq (α := ℝ) 0 (0 x)
⊢ logMap (HSMul.hSMul (β := mixedSpace K) c 1) x = 0 x
have h₁₄ : Eq (α := ℝ) 0 0
Tactic: rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]