awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hden0 :
  Ne (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R) : FractionRing R)
    (0 : FractionRing R)
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) hden0
hdenUnit :
  IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I.num : FractionalIdeal R⁰ (FractionRing R)) ↔ IsUnit I
have obtain : ∀ (c : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
  (hc :
    (↑c : FractionalIdeal R⁰ (FractionRing R)) =
      spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R))),
  IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I.num : FractionalIdeal R⁰ (FractionRing R)) ↔ IsUnit I
Tactic: obtain ⟨c, hc⟩ := hdenUnit
Cleared hypotheses: hdenUnit
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hden0 :
  Ne (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R) : FractionRing R)
    (0 : FractionRing R)
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) hden0
c : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
hc :
  (↑c : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R))
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I.num : FractionalIdeal R⁰ (FractionRing R)) ↔ IsUnit I
have rw : IsUnit
    (HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      I) ↔
  IsUnit I
Tactic: rw [← den_mul_self_eq_num', ← hc, Units.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hden0 :
  Ne (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R) : FractionRing R)
    (0 : FractionRing R)
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) hden0
c : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
hc :
  (↑c : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R))
rw :
  IsUnit
      (HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        I) ↔
    IsUnit I
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I.num : FractionalIdeal R⁰ (FractionRing R)) ↔ IsUnit I
have rw₁ : IsUnit ((↑c : FractionalIdeal R⁰ (FractionRing R)) * I) ↔ IsUnit I
Tactic: rw [← den_mul_self_eq_num', ← hc, Units.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hden0 :
  Ne (α := FractionRing R) ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R) : FractionRing R)
    (0 : FractionRing R)
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) hden0
c : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
hc :
  (↑c : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R))
rw :
  IsUnit
      (HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑I.den : R)) :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        I) ↔
    IsUnit I
rw₁ : IsUnit ((↑c : FractionalIdeal R⁰ (FractionRing R)) * I) ↔ IsUnit I
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I.num : FractionalIdeal R⁰ (FractionRing R)) ↔ IsUnit I
have rw₂ : IsUnit I ↔ IsUnit I
Tactic: rw [← den_mul_self_eq_num', ← hc, Units.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hI : I ≠ 0
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I.num
have rwa : I.num ≠ 0
Tactic: rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, FractionalIdeal.num_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hI : I ≠ 0
rwa : I.num ≠ 0
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I.num
have rwa₁ : ¬I.num = 0
Tactic: rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, FractionalIdeal.num_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : FractionalIdeal (R := R) R⁰ (FractionRing R)
hI : I ≠ 0
rwa : I.num ≠ 0
rwa₁ : ¬I.num = 0
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I.num
have rwa₂ : ¬I = 0
Tactic: rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, FractionalIdeal.num_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
have rw : ∃ (x : (FractionRing R)ˣ),
  HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
      ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ) x :
        (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
    (FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
        (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) sorry)
Tactic: rw [← ClassGroup.mk_mk0 (FractionRing R), eq_comm, ClassGroup.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ ∃ (x : (FractionRing R)ˣ),
    HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
        ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ) x :
          (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
      (FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯)
have fd_ne_zero : Ne (α := FractionRing R)
  ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R) :
    FractionRing R)
  (0 : FractionRing R)
Tactic: have fd_ne_zero : (algebraMap R (FractionRing R)) I.1.den ≠ 0 := by
    exact IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (SetLike.coe_mem _)
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
fd_ne_zero :
  Ne (α := FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R) :
      FractionRing R)
    (0 : FractionRing R)
⊢ ∃ (x : (FractionRing R)ˣ),
    HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
        ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ) x :
          (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
      (FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯)
have refine : HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
    ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        (Units.mk0
          ((algebraMap R (FractionRing R) : (a : R) → FractionRing R)
            (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R))
          fd_ne_zero) :
      (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
  (FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
    (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
      (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) sorry)
Tactic: refine ⟨Units.mk0 (algebraMap R _ I.1.den) fd_ne_zero, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
fd_ne_zero :
  Ne (α := FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R) :
      FractionRing R)
    (0 : FractionRing R)
⊢ HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
      ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          (Units.mk0
            ((algebraMap R (FractionRing R) : (a : R) → FractionRing R)
              (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R))
            fd_ne_zero) :
        (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
    (FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
        (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯)
have huv : (↑(HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
        ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            (Units.mk0
              ((algebraMap R (FractionRing R) : (a : R) → FractionRing R)
                (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R))
              fd_ne_zero) :
          (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)) :
    FractionalIdeal R⁰ (FractionRing R)) =
  (↑((FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) sorry)) :
    FractionalIdeal R⁰ (FractionRing R))
Tactic: apply Units.ext
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
fd_ne_zero :
  Ne (α := FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R) :
      FractionRing R)
    (0 : FractionRing R)
⊢ (↑(HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
          ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
              (Units.mk0
                ((algebraMap R (FractionRing R) : (a : R) → FractionRing R)
                  (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R))
                fd_ne_zero) :
            (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)) :
      FractionalIdeal R⁰ (FractionRing R)) =
    (↑((FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
            (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯)) :
      FractionalIdeal R⁰ (FractionRing R))
have huv : HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        ((algebraMap R (FractionRing R) : (a : R) → FractionRing R)
          (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R)) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    (↑I : FractionalIdeal R⁰ (FractionRing R)) =
  (↑((FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) sorry)) :
    FractionalIdeal R⁰ (FractionRing R))
Tactic: rw [mul_comm, val_mul, coe_toPrincipalIdeal, val_mk0]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
b : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ ∃ (a : ↥(Ideal R)⁰),
    Eq (α := ClassGroup R) ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) a : ClassGroup R)
      (Quot.mk
          (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
            (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
          I :
        Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
          (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
            (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
have mk : Eq (α := ClassGroup R)
  ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
        (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) sorry) :
    ClassGroup R)
  (Quot.mk
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
      I :
    Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
Tactic: refine ⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
b : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯) :
      ClassGroup R)
    (Quot.mk
        (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
          (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
        I :
      Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
          (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
have mk : Eq (α := ClassGroup R)
  ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
  (Quot.mk
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
      I :
    Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
Tactic: rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
b : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
mk :
  Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (Quot.mk
        (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
          (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
        I :
      Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
          (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
⊢ Eq (α := ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R)
        (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x)
          (integralRep (↑I : FractionalIdeal R⁰ (FractionRing R))) ⋯) :
      ClassGroup R)
    (Quot.mk
        (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
          (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
        I :
      Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
          (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
have mk₁ : Eq (α := ClassGroup R)
  ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
  ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
Tactic: rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Eq.{u_1 + 1} (α := ClassGroup R) ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)
      (1 : ClassGroup R) ↔
    (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
have rw : Eq.{u_2 + 1} (α :=
    HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
      Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K)))
    ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I) :
      HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K)))
    ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range) 1 :
      HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))) ↔
  (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
Tactic: rw [← (ClassGroup.equiv K).injective.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Eq.{u_2 + 1} (α :=
      HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K)))
      ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
          ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I) :
        HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
          Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K)))
      ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range) 1 :
        HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
          Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))) ↔
    (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
have simp : (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
  (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
Tactic: simp only [equiv_mk, canonicalEquiv_self, RingEquiv.coe_mulEquiv_refl, QuotientGroup.mk'_apply,
    map_one, QuotientGroup.eq_one_iff, MonoidHom.mem_range, Units.ext_iff,
    coe_toPrincipalIdeal, coe_mapEquiv, MulEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
h : ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
x : Kˣ
hx : spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ (↑x : K)
have rw : Eq (α := Submodule R K) (↑(spanSingleton R⁰ (↑x : K)) : Submodule R K) (R ∙ (↑x : K))
Tactic: rw [← hx, coe_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
h : ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
x : Kˣ
hx : spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
rw : Eq (α := Submodule R K) (↑(spanSingleton R⁰ (↑x : K)) : Submodule R K) (R ∙ (↑x : K))
⊢ (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ (↑x : K)
have rw₁ : Eq (α := Submodule R K) (R ∙ (↑x : K)) (R ∙ (↑x : K))
Tactic: rw [← hx, coe_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
have refine : (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal →
  ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
Tactic: refine ⟨fun ⟨x, hx⟩ => ⟨⟨x, by rw [← hx, coe_spanSingleton]⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
hI : (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
have obtain : ∀ (x : K) (hx : (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ x),
  ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
Tactic: obtain ⟨x, hx⟩ := @Submodule.IsPrincipal.principal _ _ _ _ _ _ hI