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 b : (↑(integerSet K) : Type u_1)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ (ζ : ↥(torsion K)), ζ • a = b
have simp_rw : (∃ (u : (↥(𝓞 K)⁰)ˣ),
    HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
          mixedSpace K)
        (↑a : mixedSpace K) =
      (↑b : mixedSpace K)) ↔
  ∃ (ζ : ↥(torsion K)), (↑ζ : (𝓞 K)ˣ) • (↑a : mixedSpace K) = (↑b : mixedSpace K)
Tactic: simp_rw [integerSetToAssociates_apply, Associates.quotient_mk_eq_mk,
    Associates.mk_eq_mk_iff_associated, Associated, mul_comm, Subtype.ext_iff,
    RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul, map_mul,
    mixedEmbedding_preimageOfMemIntegerSet, integerSetTorsionSMul_smul_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : (↑(integerSet K) : Type u_1)
⊢ (∃ (u : (↥(𝓞 K)⁰)ˣ),
      HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
            mixedSpace K)
          (↑a : mixedSpace K) =
        (↑b : mixedSpace K)) ↔
    ∃ (ζ : ↥(torsion K)), (↑ζ : (𝓞 K)ˣ) • (↑a : mixedSpace K) = (↑b : mixedSpace K)
have refine : (∃ (u : (↥(𝓞 K)⁰)ˣ),
    HMul.hMul (α := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
          mixedSpace K)
        (↑a : mixedSpace K) =
      (↑b : mixedSpace K)) →
  ∀ (u : (↥(𝓞 K)⁰)ˣ)
    (h :
      HMul.hMul (α := mixedSpace K)
          ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑u : ↥(𝓞 K)⁰) : 𝓞 K)) :
            mixedSpace K)
          (↑a : mixedSpace K) =
        (↑b : mixedSpace K)),
    Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
      ((unitsNonZeroDivisorsEquiv : (a : (↥(𝓞 K)⁰)ˣ) → (𝓞 K)ˣ) u : (𝓞 K)ˣ)
Tactic: refine ⟨fun ⟨u, h⟩ ↦  ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩,
    fun ⟨⟨u, _⟩, h⟩ ↦ ⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩
-- 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 : ℝ
⊢ Eq (α := Setoid (↑(integerSet K) : Type u_1)) (Setoid.ker (integerSetToAssociates K))
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1))
have a : ∀ (a b : (↑(integerSet K) : Type u_1)),
  (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
Tactic: ext a b
-- 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)
⊢ (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
have a₁ : integerSetToAssociates K a = integerSetToAssociates K b ↔
  (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
      (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
    a b
Tactic: rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
          MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- 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)
a₁ :
  integerSetToAssociates K a = integerSetToAssociates K b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
⊢ (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
have a₂ : integerSetToAssociates K b = integerSetToAssociates K a ↔
  (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
      (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
    a b
Tactic: rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
          MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- 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)
a₁ :
  integerSetToAssociates K a = integerSetToAssociates K b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₂ :
  integerSetToAssociates K b = integerSetToAssociates K a ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
⊢ (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
have a₃ : (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔
  (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
      (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
    a b
Tactic: rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
          MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- 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)
a₁ :
  integerSetToAssociates K a = integerSetToAssociates K b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₂ :
  integerSetToAssociates K b = integerSetToAssociates K a ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₃ :
  (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
⊢ (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
have a₄ : (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔ a ∈ MulAction.orbit (↥(torsion K)) b
Tactic: rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
          MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- 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)
a₁ :
  integerSetToAssociates K a = integerSetToAssociates K b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₂ :
  integerSetToAssociates K b = integerSetToAssociates K a ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₃ :
  (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
a₄ : (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔ a ∈ MulAction.orbit (↥(torsion K)) b
⊢ (Setoid.ker (integerSetToAssociates K) : (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop) a b ↔
    (MulAction.orbitRel ↥(torsion K) (↑(integerSet K) : Type u_1) :
        (↑(integerSet K) : Type u_1) → (↑(integerSet K) : Type u_1) → Prop)
      a b
have a₅ : (∃ (ζ : ↥(torsion K)), ζ • b = a) ↔ ∃ (x : ↥(torsion K)), x • b = a
Tactic: rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a,
          MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
-- 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 (α := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ⊥
have refine : ∀ (ζ : ↥(torsion K)) (hζ : Membership.mem (γ := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ζ), ζ = 1
Tactic: refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_
-- 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)
ζ : ↥(torsion K)
hζ : Membership.mem (γ := Subgroup ↥(torsion K)) (MulAction.stabilizer (↥(torsion K)) a) ζ
⊢ ζ = 1
have rwa : ∀ (hζ : (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) * (↑(preimageOfMemIntegerSet a) : 𝓞 K) = (↑(preimageOfMemIntegerSet a) : 𝓞 K)),
  (↑(preimageOfMemIntegerSet a) : 𝓞 K) ≠ 0
Tactic: rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe,
    unitSMul_smul, ← mixedEmbedding_preimageOfMemIntegerSet, ← map_mul,
    (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀,
    Units.val_eq_one, OneMemClass.coe_eq_one] at hζ
Cleared hypotheses: hζ
-- 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 : Quotient (α := (↑(integerSet K) : Type u_1)) (MulAction.orbitRel ↥(Units.torsion K) (↑(integerSet K) : Type u_1))
⊢ HasQuotient.Quotient ↥(Units.torsion K) (B := Subgroup ↥(Units.torsion K))
      (MulAction.stabilizer (↥(Units.torsion K)) a.out) ≃
    ↥(Units.torsion K)
have simp_rw : HasQuotient.Quotient ↥(Units.torsion K) (B := Subgroup ↥(Units.torsion K)) ⊥ ≃ ↥(Units.torsion K)
Tactic: simp_rw [integerSetTorsionSMul_stabilizer]
-- 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 : ℝ
n : ℕ
x_1 : (↑(integerSet K) : Type u_1)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
have simp_rw : Eq (α := ℝ) (↑(intNorm x_1) : ℝ) (↑n : ℝ) ↔
  (absNorm : (a : Ideal (𝓞 K)) → ℕ)
      (↑(↑((integerSetEquiv K :
                    (a : (↑(integerSet K) : Type u_1)) →
                      { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                  x_1).1 :
            ↥(Ideal (𝓞 K))⁰) :
        Ideal (𝓞 K)) =
    n
Tactic: simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]
-- 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 : ℝ
n : ℕ
x_1 : (↑(integerSet K) : Type u_1)
simp_rw :
  Eq (α := ℝ) (↑(intNorm x_1) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
have simp_rw₁ : Eq (α := ℝ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K))) : ℝ) (↑n : ℝ) ↔
  (absNorm : (a : Ideal (𝓞 K)) → ℕ)
      (↑(↑((integerSetEquiv K :
                    (a : (↑(integerSet K) : Type u_1)) →
                      { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                  x_1).1 :
            ↥(Ideal (𝓞 K))⁰) :
        Ideal (𝓞 K)) =
    n
Tactic: simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]
-- 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 : ℝ
n : ℕ
x_1 : (↑(integerSet K) : Type u_1)
simp_rw :
  Eq (α := ℝ) (↑(intNorm x_1) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
simp_rw₁ :
  Eq (α := ℝ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K))) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
have simp_rw₂ : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K)) = n ↔
  (absNorm : (a : Ideal (𝓞 K)) → ℕ)
      (↑(↑((integerSetEquiv K :
                    (a : (↑(integerSet K) : Type u_1)) →
                      { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                  x_1).1 :
            ↥(Ideal (𝓞 K))⁰) :
        Ideal (𝓞 K)) =
    n
Tactic: simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]
-- 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 : ℝ
n : ℕ
x_1 : (↑(integerSet K) : Type u_1)
simp_rw :
  Eq (α := ℝ) (↑(intNorm x_1) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
simp_rw₁ :
  Eq (α := ℝ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K))) : ℝ) (↑n : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
simp_rw₂ :
  Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K)) = n ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑x_1 : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ) ↔
    (absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(↑((integerSetEquiv K :
                      (a : (↑(integerSet K) : Type u_1)) →
                        { I : ↥(Ideal (𝓞 K))⁰ // IsPrincipal (↑I : Ideal (𝓞 K)) } × ↥(Units.torsion K))
                    x_1).1 :
              ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) =
      n
have simp_rw₃ : Int.natAbs ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (↑(preimageOfMemIntegerSet x_1) : 𝓞 K)) = n ↔
  (absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {(↑(preimageOfMemIntegerSet x_1) : 𝓞 K)}) = n
Tactic: simp_rw [← intNorm_coe, intNorm,
        Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
⊢ Nat.card.{u_1}
        (↑{I : ↥(Ideal (𝓞 K))⁰ |
              IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n} :
          Type u_1) *
      torsionOrder K =
    Nat.card.{u_1}
      (↑{a : (↑(integerSet K) : Type u_1) |
            Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)} :
        Type u_1)
have rw : Nat.card.{u_1}
    ((↑{I : ↥(Ideal (𝓞 K))⁰ |
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) = n} :
        Type u_1) ×
      ↥(Units.torsion K)) =
  Nat.card.{u_1}
    (↑{a : (↑(integerSet K) : Type u_1) |
          Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑n : ℝ) : ℝ)} :
      Type u_1)
Tactic: rw [torsionOrder, ← Nat.card_eq_fintype_card, ← Nat.card_prod]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : (↑(idealSet K J) : Type u_1)
⊢ (↑(preimageOfMemIntegerSet (idealSetMap K J a)) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
have obtain : Membership.mem (γ := Set (mixedSpace K)) (fundamentalCone K) (↑a : mixedSpace K) →
  ∀ (x : 𝓞 K) (hx₁ : x ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K)))
    (hx₂ : (mixedEmbedding K : (a : K) → mixedSpace K) (↑x : K) = (↑a : mixedSpace K)),
    (↑(preimageOfMemIntegerSet (idealSetMap K J a)) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
Tactic: obtain ⟨_, ⟨x, hx₁, hx₂⟩⟩ := mem_idealSet.mp a.prop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x_1 x_2 : (↑(idealSet K J) : Type u_1)
h :
  Eq.{u_1 + 1} (α :=
    (↑{a : (↑(integerSet K) : Type u_1) | (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
      Type u_1))
    ((fun (a : (↑(idealSet K J) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : (↑(integerSet K) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x)
            (idealSetMap K J a) ⋯ :
          { x : (↑(integerSet K) : Type u_1) //
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x }))
      x_1)
    ((fun (a : (↑(idealSet K J) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : (↑(integerSet K) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x)
            (idealSetMap K J a) ⋯ :
          { x : (↑(integerSet K) : Type u_1) //
            Membership.mem (γ := Set (↑(integerSet K) : Type u_1))
              {a : (↑(integerSet K) : Type u_1) |
                (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))}
              x }))
      x_2)
⊢ x_1 = x_2
have h₁ : (↑x_1 : mixedSpace K) = (↑x_2 : mixedSpace K)
Tactic: simp_rw [Subtype.ext_iff, idealSetMap_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : { a : (↑(integerSet K) : Type u_1) // (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K)) }
⊢ (↑((Equiv.symm (idealSetEquiv K J) :
            (a :
                (↑{a : (↑(integerSet K) : Type u_1) |
                      (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                  Type u_1)) →
              (↑(idealSet K J) : Type u_1))
          a) :
      mixedSpace K) =
    (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K)
have rw : (↑(↑((idealSetEquiv K J :
              (a : (↑(idealSet K J) : Type u_1)) →
                (↑{a : (↑(integerSet K) : Type u_1) |
                      (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                  Type u_1))
            ((Equiv.symm (idealSetEquiv K J) :
                (a :
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1)) →
                  (↑(idealSet K J) : Type u_1))
              a)) :
        (↑(integerSet K) : Type u_1)) :
    mixedSpace K) =
  (↑(↑a : (↑(integerSet K) : Type u_1)) : mixedSpace K)
Tactic: rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]