awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ClassGroup
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
rw₂ rw₃ : IsUnit I ↔ IsUnit I
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I.num : FractionalIdeal R⁰ (FractionRing R)) ↔ IsUnit I

Tactic:
rw [← den_mul_self_eq_num', ← hc, Units.isUnit_units_mul]

Premises used: Units.isUnit_units_mul, FractionalIdeal.den_mul_self_eq_num'
-- Module: Mathlib.RingTheory.ClassGroup
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
rwa₂ rwa₃ rwa₄ rwa₅ : ¬I = 0
⊢ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I.num

Tactic:
rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, FractionalIdeal.num_eq_zero_iff]

Premises used: ne_eq, mem_nonZeroDivisors_iff_ne_zero, FractionalIdeal.num_eq_zero_iff
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
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))) ⋯)
⊢ 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)

Tactic:
rw [← ClassGroup.mk_mk0 (FractionRing R), eq_comm, ClassGroup.mk_eq_mk]

Premises used: FractionRing, eq_comm, ClassGroup.mk_mk0, ClassGroup.mk_eq_mk
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Ne (α := FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R) :
      FractionRing R)
    (0 : FractionRing R)

Tactic:
IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (SetLike.coe_mem _)

Premises used: SetLike.coe_mem, IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Ne (α := FractionRing R)
    ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) (↑(↑I : FractionalIdeal R⁰ (FractionRing R)).den : R) :
      FractionRing R)
    (0 : FractionRing R)

Tactic:
exact IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (SetLike.coe_mem _)

Premises used: SetLike.coe_mem, IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ 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 _)
-- Module: Mathlib.RingTheory.ClassGroup
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))) ⋯)

Tactic:
⟨Units.mk0 (algebraMap R _ I.1.den) fd_ne_zero, ?_⟩

Premises used: Units.val, Algebra.algebraMap, Units.mk0, FractionalIdeal.den, Exists.intro, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.ClassGroup
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)
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))) ⋯)
⊢ ∃ (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))) ⋯)

Tactic:
refine ⟨Units.mk0 (algebraMap R _ I.1.den) fd_ne_zero, ?_⟩
-- Module: Mathlib.RingTheory.ClassGroup
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)
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))) ⋯)) :
      FractionalIdeal R⁰ (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))) ⋯)

Tactic:
apply Units.ext

Premises used: Units.ext
-- Module: Mathlib.RingTheory.ClassGroup
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)
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))) ⋯)) :
      FractionalIdeal R⁰ (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))

Tactic:
rw [mul_comm, val_mul, coe_toPrincipalIdeal, val_mk0]

Premises used: coe_toPrincipalIdeal, mul_comm, Units.val_mk0, Units.val_mul
-- Module: Mathlib.RingTheory.ClassGroup
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))
      (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))) ⋯)) :
      FractionalIdeal R⁰ (FractionRing R))

Tactic:
FractionalIdeal.den_mul_self_eq_num' R⁰ (FractionRing R) I

Premises used: Units.val, FractionalIdeal.num, FractionRing, nonZeroDivisors, ClassGroup.integralRep, Submodule.comap, FractionalIdeal.den_mul_self_eq_num', FractionalIdeal.coeIdeal
-- Module: Mathlib.RingTheory.ClassGroup
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))
      (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))) ⋯)) :
      FractionalIdeal R⁰ (FractionRing R))

Tactic:
exact FractionalIdeal.den_mul_self_eq_num' R⁰ (FractionRing R) I

Premises used: Units.val, FractionRing, nonZeroDivisors, FractionalIdeal.den_mul_self_eq_num'
-- Module: Mathlib.RingTheory.ClassGroup
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))

Tactic:
⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩

Premises used: Units.val, Units.ne_zero, Subtype.mk, ClassGroup.integralRep, Exists.intro, ClassGroup.integralRep_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.ClassGroup
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)
    ((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))
⊢ ∃ (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))

Tactic:
refine ⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩
-- Module: Mathlib.RingTheory.ClassGroup
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))
mk₁ 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)
⊢ 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))

Tactic:
rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]

Premises used: ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk
-- Module: Mathlib.RingTheory.ClassGroup
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)ˣ
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
⊢ 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

Tactic:
rw [← (ClassGroup.equiv K).injective.eq_iff]

Premises used: Function.Injective.eq_iff, ClassGroup.equiv, MulEquiv.injective
-- Module: Mathlib.RingTheory.ClassGroup
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)ˣ
simp :
  (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
⊢ 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:
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]

Premises used: Units.ext_iff, coe_toPrincipalIdeal, QuotientGroup.mk'_apply, MonoidHom.mem_range, map_one, FractionalIdeal.canonicalEquiv_self, QuotientGroup.eq_one_iff, Units.coe_mapEquiv, ClassGroup.equiv_mk, RingEquiv.coe_mulEquiv_refl, MulEquiv.refl_apply
-- Module: Mathlib.RingTheory.ClassGroup
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))
rw₁ rw₂ : Eq (α := Submodule R K) (R ∙ (↑x : K)) (R ∙ (↑x : K))
⊢ (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ (↑x : K)

Tactic:
rw [← hx, coe_spanSingleton]

Premises used: FractionalIdeal.coe_spanSingleton
-- Module: Mathlib.RingTheory.ClassGroup
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)ˣ
refine :
  (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal →
    ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal

Tactic:
refine ⟨fun ⟨x, hx⟩ => ⟨⟨x, by rw [← hx, coe_spanSingleton]⟩⟩, ?_⟩
-- Module: Mathlib.RingTheory.ClassGroup
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
obtain :
  ∀ (x : K) (hx : (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ x),
    ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
obtain ⟨x, hx⟩ := @Submodule.IsPrincipal.principal _ _ _ _ _ _ hI

Premises used: Submodule.IsPrincipal.principal
-- Module: Mathlib.RingTheory.ClassGroup
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
hx : (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ x
a :
  Eq.{u_2 + 1} (α := Submodule R K)
    ((fun (a : { I : Submodule R K // IsFractional R⁰ I }) ↦ (↑a : Submodule R K)) (↑I : FractionalIdeal R⁰ K))
    ((fun (a : { I : Submodule R K // IsFractional R⁰ I }) ↦ (↑a : Submodule R K)) (spanSingleton R⁰ x))
⊢ (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x

Tactic:
apply Subtype.coe_injective

Premises used: Subtype.coe_injective