awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
rw :
  (∃ (z : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      Membership.mem (γ := Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
          (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) z ∧
        HMul.hMul (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
            ((Units.map
                    (↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R)) :
                      FractionalIdeal R⁰ (FractionRing R) →* FractionalIdeal R⁰ (FractionRing R)) :
                  (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
                I :
              (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
            z =
          (Units.map
                (↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R)) :
                  FractionalIdeal R⁰ (FractionRing R) →* FractionalIdeal R⁰ (FractionRing R)) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            J) ↔
    ∃ (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))ˣ) =
        J
⊢ Eq (α := ClassGroup R)
      ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
      ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) J : ClassGroup 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))ˣ) =
        J

Tactic:
rw [mk_def, mk_def, QuotientGroup.mk'_eq_mk']

Premises used: QuotientGroup.mk'_eq_mk', ClassGroup.mk_def
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ (∃ (z : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      Membership.mem (γ := Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
          (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) z ∧
        HMul.hMul (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
            ((Units.map
                    (↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R)) :
                      FractionalIdeal R⁰ (FractionRing R) →* FractionalIdeal R⁰ (FractionRing R)) :
                  (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
                I :
              (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
            z =
          (Units.map
                (↑(canonicalEquiv R⁰ (FractionRing R) (FractionRing R)) :
                  FractionalIdeal R⁰ (FractionRing R) →* FractionalIdeal R⁰ (FractionRing R)) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            J) ↔
    ∃ (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))ˣ) =
        J

Tactic:
simp [RingEquiv.coe_monoidHom_refl, MonoidHom.mem_range, -toPrincipalIdeal_eq_iff]

Premises used: MonoidHom.mem_range, toPrincipalIdeal_eq_iff, RingEquiv.coe_monoidHom_refl
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal 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))ˣ) =
        J) ↔
    ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ Eq (α := ClassGroup R)
      ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
      ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) J : ClassGroup R) ↔
    ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
rw [ClassGroup.mk_eq_mk]

Premises used: ClassGroup.mk_eq_mk
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
mp :
  (∃ (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))ˣ) =
        J) →
    ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
mpr :
  (∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J') →
    ∃ (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))ˣ) =
        J
⊢ (∃ (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))ˣ) =
        J) ↔
    ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
constructor
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x : (FractionRing R)ˣ
hJ :
  (↑(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 R⁰ (FractionRing R)) =
    (↑J' : FractionalIdeal R⁰ (FractionRing R))
⊢ Ideal.span {(sec R⁰ (↑x : FractionRing R)).1} * I' = Ideal.span {(↑(sec R⁰ (↑x : FractionRing R)).2 : R)} * J'

Tactic:
rw [Units.val_mul, hI, coe_toPrincipalIdeal, mul_comm,
      spanSingleton_mul_coeIdeal_eq_coeIdeal] at hJ

Premises used: coe_toPrincipalIdeal, FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal, mul_comm, Units.val_mul
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x : (FractionRing R)ˣ
hJ : Ideal.span {(sec R⁰ (↑x : FractionRing R)).1} * I' = Ideal.span {(↑(sec R⁰ (↑x : FractionRing R)).2 : R)} * J'
⊢ ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
⟨_, _, sec_fst_ne_zero x.ne_zero,
      sec_snd_ne_zero (R := R) le_rfl (x : FractionRing R), hJ⟩

Premises used: Units.val, IsLocalization.sec_snd_ne_zero, le_rfl, Units.ne_zero, And.intro, Exists.intro, IsLocalization.sec_fst_ne_zero
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x : (FractionRing R)ˣ
hJ : Ideal.span {(sec R⁰ (↑x : FractionRing R)).1} * I' = Ideal.span {(↑(sec R⁰ (↑x : FractionRing R)).2 : R)} * J'
⊢ ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

Tactic:
exact ⟨_, _, sec_fst_ne_zero x.ne_zero,
      sec_snd_ne_zero (R := R) le_rfl (x : FractionRing R), hJ⟩
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))

Tactic:
simpa only [isUnit_iff_ne_zero, ne_eq, mk'_eq_zero_iff_eq_zero] using hx

Premises used: isUnit_iff_ne_zero, ne_eq, IsFractionRing.mk'_eq_zero_iff_eq_zero
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
⊢ IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))

Tactic:
have : IsUnit (mk' (FractionRing R) x ⟨y, mem_nonZeroDivisors_of_ne_zero hy⟩) := by
      simpa only [isUnit_iff_ne_zero, ne_eq, mk'_eq_zero_iff_eq_zero] using hx
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this :
  IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))
⊢ ∃ (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))ˣ) =
      J

Tactic:
⟨this.unit, ?_⟩

Premises used: Exists.intro, IsUnit.unit
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this :
  IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))
mpr :
  HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
      ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          this.unit :
        (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
    J
⊢ ∃ (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))ˣ) =
      J

Tactic:
refine ⟨this.unit, ?_⟩
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this :
  IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))
mpr :
  spanSingleton R⁰ (↑this.unit : FractionRing R) * (↑I : FractionalIdeal R⁰ (FractionRing R)) =
    (↑J : FractionalIdeal R⁰ (FractionRing R))
⊢ HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
      ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          this.unit :
        (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
    J

Tactic:
rw [mul_comm, ← Units.val_inj, Units.val_mul, coe_toPrincipalIdeal]

Premises used: coe_toPrincipalIdeal, Units.val_inj, mul_comm, Units.val_mul
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this :
  IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰
        (mk' (M := R⁰) (FractionRing R) x
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯)))
      (↑I' : FractionalIdeal R⁰ (FractionRing R)) =
    (↑J' : FractionalIdeal R⁰ (FractionRing R))

Tactic:
(mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h

Premises used: Iff.mpr, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, FractionRing, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
hJ : (↑J : FractionalIdeal R⁰ (FractionRing R)) = (↑J' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * J'
this :
  IsUnit (M := FractionRing R)
    (mk' (M := R⁰) (FractionRing R) x
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) x) y ⋯))
⊢ spanSingleton R⁰ (↑this.unit : FractionRing R) * (↑I : FractionalIdeal R⁰ (FractionRing R)) =
    (↑J : FractionalIdeal R⁰ (FractionRing R))

Tactic:
convert!
      (mk'_mul_coeIdeal_eq_coeIdeal (FractionRing R) <| mem_nonZeroDivisors_of_ne_zero hy).2 h

Premises used: Iff.mpr, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, FractionRing, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
rw :
  (∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = HMul.hMul (α := Ideal R) (Ideal.span {y}) ⊤) ↔
    ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}
rw₁ :
  Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑1 : FractionalIdeal R⁰ (FractionRing R))
    (↑⊤ : FractionalIdeal R⁰ (FractionRing R))
rw₂ : Ideal R
⊢ Eq (α := ClassGroup R)
      ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
      (1 : ClassGroup R) ↔
    ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)),
    ClassGroup.mk_eq_mk_of_coe_ideal hI]

Premises used: ClassGroup.mk_eq_mk_of_coe_ideal, FractionRing, map_one, ClassGroup.mk
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
⊢ Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑1 : FractionalIdeal R⁰ (FractionRing R))
    (↑⊤ : FractionalIdeal R⁰ (FractionRing R))

Tactic:
rfl
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
mp :
  (∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = HMul.hMul (α := Ideal R) (Ideal.span {y}) ⊤) →
    ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}
mpr :
  (∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}) →
    ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = HMul.hMul (α := Ideal R) (Ideal.span {y}) ⊤
⊢ (∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = HMul.hMul (α := Ideal R) (Ideal.span {y}) ⊤) ↔
    ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
constructor
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = HMul.hMul (α := Ideal R) (Ideal.span {y}) ⊤
⊢ Ideal.span {x} * I' = Ideal.span {y}

Tactic:
rw [Ideal.mul_top] at h

Premises used: Ideal.mul_top
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
mp :
  ∀ (i : R) (_hi : i ∈ I') (hy : x * i ≠ 0) (h : Ideal.span {x} * I' = Ideal.span {x * i}),
    ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}
⊢ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
      ⟨i, _hi, rfl⟩

Premises used: Eq.ge, Ideal.span_singleton_le_iff_mem, Iff.mp, Ideal.mem_span_singleton_mul, rfl
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : Ideal.span {x} * I' = Ideal.span {x * i}
⊢ I' = Ideal.span {i}

Tactic:
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h

Premises used: Ideal.span_singleton_mul_right_inj, Ideal.span_singleton_mul_span_singleton
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ i ≠ 0

Tactic:
grobner
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
exact ⟨i, by grobner, h⟩
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑(Ideal.span {x}) : FractionalIdeal R⁰ (FractionRing R))
rw : HMul.hMul (α := Ideal R) ⊤ (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
rw₁ : Ideal.span {x} = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
rw₂ rw₃ : Eq (α := Ideal R) (Ideal.span {x}) (Ideal.span {x})
⊢ HMul.hMul (α := Ideal R) (Ideal.span {1}) (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤

Tactic:
rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]

Premises used: Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑(Ideal.span {x}) : FractionalIdeal R⁰ (FractionRing R))
⊢ ∃ (x_1 : R) (y : R),
    x_1 ≠ 0 ∧
      y ≠ 0 ∧ HMul.hMul (α := Ideal R) (Ideal.span {x_1}) (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {y}) ⊤

Tactic:
exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩
-- 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
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), P ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ I =
    (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
      ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I)

Tactic:
simp [← Units.val_inj]

Premises used: Units.val_inj
-- 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
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), P ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
have :
  ∀
    (this :
      I =
        (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K)) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I)),
    P (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
⊢ P (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)

Tactic:
have : I = (Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv)
      (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv I) := by
      simp [← Units.val_inj]