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
a : (↑(integerSet K) : Type u_1)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw : Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw₁ : Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₁ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw₂ : Eq (α := ℝ) ((↑(↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℚ) : ℝ) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₁ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₂ :
  Eq (α := ℝ) ((↑(↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℚ) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw₃ : Eq (α := ℝ) ((↑|(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)) : ℚ)| : ℝ) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₁ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₂ :
  Eq (α := ℝ) ((↑(↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℚ) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ) ((↑|(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)) : ℚ)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw₄ : Eq (α := ℝ) ((↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K)| : ℝ) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₁ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₂ :
  Eq (α := ℝ) ((↑(↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℚ) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ) ((↑|(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)) : ℚ)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₄ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw₅ : Eq (α := ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K) : mixedSpace K) :
    ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : (↑(integerSet K) : Type u_1)
rw :
  Eq (α := ℝ) ((↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K))) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₁ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₂ :
  Eq (α := ℝ) ((↑(↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)| : ℚ) : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ) ((↑|(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet a) : 𝓞 K)) : ℚ)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₄ :
  Eq (α := ℝ) ((↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K)| : ℝ) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
rw₅ :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑(preimageOfMemIntegerSet a) : 𝓞 K) : K) : mixedSpace K) :
      ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
⊢ Eq (α := ℝ) ((↑(intNorm a) : ℝ) : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
have rw₆ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
Tactic: rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]
-- 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
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)
have rw : Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
  (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]
-- 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
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
rw :
  Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
    (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)
have rw₁ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
  ((↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ) : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]
-- 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
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
rw :
  Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
    (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
rw₁ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ) : ℝ)
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)
have rw₂ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]
-- 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
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
rw :
  Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
    (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
rw₁ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ) : ℝ)
rw₂ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)
have rw₃ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑((fun (m : ↥(torsion K)) ↦ m • b) u) : mixedSpace K) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]
-- 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
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
rw :
  Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
    (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
rw₁ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ) : ℝ)
rw₂ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑((fun (m : ↥(torsion K)) ↦ m • b) u) : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)
have rw₄ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((↑u : (𝓞 K)ˣ) • (↑b : mixedSpace K)) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]
-- 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
c : ℝ
a b : (↑(integerSet K) : Type u_1)
h : a ≈ b
u : ↥(torsion K)
hu : (fun (m : ↥(torsion K)) ↦ m • b) u = a
rw :
  Eq (α := ℝ) (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a) : ℝ)
    (↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ)
rw₁ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((↑((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b) : ℝ) : ℝ)
rw₂ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
rw₃ :
  Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑((fun (m : ↥(torsion K)) ↦ m • b) u) : mixedSpace K) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
rw₄ :
  Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((↑u : (𝓞 K)ˣ) • (↑b : mixedSpace K)) : ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
⊢ Eq (α := ℕ) ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) a)
    ((fun (x : (↑(integerSet K) : Type u_1)) ↦ intNorm x) b)
have rw₅ : Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
  ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑b : mixedSpace K) : ℝ)
Tactic: rw [← Nat.cast_inj (R := ℝ), intNorm_coe, intNorm_coe, ← hu, integerSetTorsionSMul_smul_coe,
      norm_unit_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ (u : (𝓞 K)ˣ),
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
have refine : Ne (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K) (0 : mixedSpace K)
Tactic: refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ (a : (↑(integerSet K) : Type u_1)),
    integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x
have mk : ∀ (u : (𝓞 K)ˣ)
  (hu :
    Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
      (HSMul.hSMul (β := mixedSpace K) u
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))),
  ∃ (a : (↑(integerSet K) : Type u_1)),
    integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x
Tactic: obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K := by
    refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
    exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
⊢ ∃ (a : (↑(integerSet K) : Type u_1)),
    integerSetToAssociates K a = Quot.mk (⇑(Associated.setoid ↥(𝓞 K)⁰) : ↥(𝓞 K)⁰ → ↥(𝓞 K)⁰ → Prop) x
have mk : preimageOfMemIntegerSet
      (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
        (HSMul.hSMul (β := mixedSpace K) u
          ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
        hu) *
    (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) =
  x
Tactic: refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩,
    Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
⊢ preimageOfMemIntegerSet
        (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
          (HSMul.hSMul (β := mixedSpace K) u
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
          hu) *
      (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) =
    x
have mk : (↑(preimageOfMemIntegerSet
          (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
            (HSMul.hSMul (β := mixedSpace K) u
              ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
            hu) *
        (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
    𝓞 K) =
  (↑x : 𝓞 K)
Tactic: simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
    Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
mk :
  (↑(preimageOfMemIntegerSet
            (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
              (HSMul.hSMul (β := mixedSpace K) u
                ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
              hu) *
          (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
      𝓞 K) =
    (↑x : 𝓞 K)
⊢ preimageOfMemIntegerSet
        (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
          (HSMul.hSMul (β := mixedSpace K) u
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
          hu) *
      (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) =
    x
have mk₁ : (↑(↑(preimageOfMemIntegerSet
              (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                (HSMul.hSMul (β := mixedSpace K) u
                  ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                hu) *
            (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
        𝓞 K) :
    K) =
  (↑(↑x : 𝓞 K) : K)
Tactic: simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
    Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
mk :
  (↑(preimageOfMemIntegerSet
            (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
              (HSMul.hSMul (β := mixedSpace K) u
                ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
              hu) *
          (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
      𝓞 K) =
    (↑x : 𝓞 K)
mk₁ :
  (↑(↑(preimageOfMemIntegerSet
                (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                  (HSMul.hSMul (β := mixedSpace K) u
                    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                  hu) *
              (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
          𝓞 K) :
      K) =
    (↑(↑x : 𝓞 K) : K)
⊢ preimageOfMemIntegerSet
        (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
          (HSMul.hSMul (β := mixedSpace K) u
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
          hu) *
      (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) =
    x
have mk₂ : Eq (α := mixedSpace K)
  ((mixedEmbedding K : (a : K) → mixedSpace K)
      (↑(↑(preimageOfMemIntegerSet
                  (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                    (HSMul.hSMul (β := mixedSpace K) u
                      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                    hu) *
                (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
            𝓞 K) :
        K) :
    mixedSpace K)
  ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
Tactic: simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
    Units.mul_inv_cancel_right]