awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) z
obtain :
  ∀ (z : R) (hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)),
    Membership.mem (γ := Ideal R) (span {x}) (b * (g * z))
⊢ Membership.mem (γ := Ideal R) (span {x}) (b * z)

Tactic:
obtain ⟨z, rfl⟩ := mem_span_singleton.mp hz

Premises used: Iff.mp, Ideal.mem_span_singleton, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
rw : x ∣ b * g * z
⊢ Membership.mem (γ := Ideal R) (span {x}) (b * (g * z))

Tactic:
rw [mem_span_singleton, ← mul_assoc]

Premises used: mul_assoc, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
h : x ∣ b * g
⊢ x ∣ b * g * z

Tactic:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
h : x ∣ HMul.hMul (α := R) ((normalize : (a : R) → R) b : R) g
⊢ x ∣ b * g

Tactic:
suffices x ∣ normalize b * g from this.trans ((associated_normalize b).mul_right g).dvd'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
h : ∀ b_1 ∈ T, x ∣ b * id b_1
⊢ x ∣ HMul.hMul (α := R) ((normalize : (a : R) → R) b : R) g

Tactic:
rw [← Finset.gcd_mul_left, Finset.dvd_gcd_iff]

Premises used: Finset.gcd_mul_left, Finset.dvd_gcd_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
c : R
hc : c ∈ T
h : b * id c ∈ J * K
⊢ x ∣ b * id c

Tactic:
rw [← mem_span_singleton, span, ← hJK]

Premises used: Ideal.span, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
c : R
hc : c ∈ T
⊢ b * id c ∈ J * K

Tactic:
mul_mem_mul hb (hTK hc)

Premises used: Set.Mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
J : Ideal R
this : NormalizedGCDMonoid R := Classical.choice ⋯
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : (↑T : Set R) ⊆ (↑K : Set R)
K' : Ideal R := span (↑T : Set R)
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : Membership.mem (γ := Ideal R) (span {g}) (g * z)
c : R
hc : c ∈ T
⊢ b * id c ∈ J * K

Tactic:
exact mul_mem_mul hb (hTK hc)

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
obtain :
  ∀ (a : R) (K : Ideal R) (ha0 : a ≠ 0)
    (h :
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
          FractionalIdeal (R := R) R⁰ (FractionRing R))
          (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
            FractionalIdeal (R := R) R⁰ (FractionRing R))
          ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))),
    Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨a, K, ha0, h⟩ := exists_eq_spanSingleton_mul (I : FractionalIdeal R⁰ (FractionRing R))⁻¹

Premises used: Inv.inv, FractionalIdeal.exists_eq_spanSingleton_mul, FractionalIdeal.coeIdeal
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
rw :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
⊢ Eq (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑(I * K) : FractionalIdeal R⁰ (FractionRing R))
    (↑(span {a}) : FractionalIdeal R⁰ (FractionRing R))

Tactic:
rw [coeIdeal_mul, coeIdeal_span_singleton]

Premises used: FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.coeIdeal_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
rw :
  ∀
    (hI :
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
          (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
        1)
    (a : R) (K : Ideal R) (ha0 : a ≠ 0)
    (h :
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
          FractionalIdeal (R := R) R⁰ (FractionRing R))
          (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
            FractionalIdeal (R := R) R⁰ (FractionRing R))
          ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))),
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
        (↑K : FractionalIdeal R⁰ (FractionRing R)) =
      spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)

Tactic:
rw [← mul_inv_cancel_iff_isUnit] at hI

Premises used: FractionalIdeal.mul_inv_cancel_iff_isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    1
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a))⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) =
    1

Tactic:
have ha0' := spanSingleton_mul_inv (R₁ := R) (FractionRing R)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
          (mem_nonZeroDivisors_iff_ne_zero.mpr ha0))
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    1
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
ha0' :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a))⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) =
    1
⊢ Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    ((fun (t : FractionalIdeal (R := R) R⁰ (FractionRing R)) ↦
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
            FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          t)
      (HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))))
    ((fun (t : FractionalIdeal (R := R) R⁰ (FractionRing R)) ↦
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
            FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          t)
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹)

Tactic:
replace h :=
        congrArg
          (fun t =>
            spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * I * t)
          h.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ I * K = span {a}

Tactic:
have hIK : I * K = Ideal.span ({a} : Set R) :=
    (coeIdeal_inj (K := FractionRing R)).mp <| by
      rw [coeIdeal_mul, coeIdeal_span_singleton]
      rw [← mul_inv_cancel_iff_isUnit] at hI
      have ha0' := spanSingleton_mul_inv (R₁ := R) (FractionRing R)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
          (mem_nonZeroDivisors_iff_ne_zero.mpr ha0))
      replace h :=
        congrArg
          (fun t =>
            spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * I * t)
          h.symm
      dsimp only at h
      rwa [mul_mul_mul_comm, ← spanSingleton_inv, ha0', one_mul, mul_assoc, hI, mul_one] at h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
⊢ Submodule.IsPrincipal I

Tactic:
isPrincipal_of_exists_mul_ne_zero_isPrincipal (J := I) ?_

Premises used: NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
refine : ∃ (K : Ideal R), I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)
⊢ Submodule.IsPrincipal I

Tactic:
refine isPrincipal_of_exists_mul_ne_zero_isPrincipal (J := I) ?_

Premises used: NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
⊢ ∃ (K : Ideal R), I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)

Tactic:
⟨K, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
refine_1 : I * K ≠ 0
refine_2 : Submodule.IsPrincipal (I * K)
⊢ ∃ (K : Ideal R), I * K ≠ 0 ∧ Submodule.IsPrincipal (I * K)

Tactic:
refine ⟨K, ?_, ?_⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
⊢ I * K ≠ 0

Tactic:
simp [hIK, ha0]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
a : R
K : Ideal R
ha0 : a ≠ 0
h :
  (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R))
hIK : I * K = span {a}
⊢ Submodule.IsPrincipal (I * K)

Tactic:
simpa [hIK] using (inferInstance : (Ideal.span {a}).IsPrincipal)

Premises used: inferInstance
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I : FractionalIdeal R⁰ (FractionRing R)).num
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑J : FractionalIdeal R⁰ (FractionRing R))

Tactic:
have hJunit : IsUnit (J : FractionalIdeal R⁰ (FractionRing R)) :=
    FractionalIdeal.isUnit_num.mpr ⟨I, rfl⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I : FractionalIdeal R⁰ (FractionRing R)).num
hJunit : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑J : FractionalIdeal R⁰ (FractionRing R))
⊢ Submodule.IsPrincipal J

Tactic:
have hJprin : J.IsPrincipal := isPrincipal_of_isUnit_fractionalIdeal J hJunit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I : FractionalIdeal R⁰ (FractionRing R)).num
hJunit : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑J : FractionalIdeal R⁰ (FractionRing R))
hJprin : Submodule.IsPrincipal J
⊢ (↑(↑I : FractionalIdeal R⁰ (FractionRing R)) : Submodule R (FractionRing R)).IsPrincipal

Tactic:
isPrincipal_of_isPrincipal_num
    (I : FractionalIdeal R⁰ (FractionRing R)) hJprin

Premises used: Units.val, FractionalIdeal.isPrincipal_of_isPrincipal_num
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
J : Ideal R := (↑I : FractionalIdeal R⁰ (FractionRing R)).num
hJunit : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑J : FractionalIdeal R⁰ (FractionRing R))
hJprin : Submodule.IsPrincipal J
⊢ (↑(↑I : FractionalIdeal R⁰ (FractionRing R)) : Submodule R (FractionRing R)).IsPrincipal

Tactic:
exact isPrincipal_of_isPrincipal_num
    (I : FractionalIdeal R⁰ (FractionRing R)) hJprin

Premises used: Units.val, FractionalIdeal.isPrincipal_of_isPrincipal_num
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
⊢ Subsingleton.{u_1 + 1} (ClassGroup R)

Tactic:
subsingleton_of_forall_eq 1 ?_

Premises used: subsingleton_of_forall_eq, OfNat.ofNat