awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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))

Tactic:
simp only [val_eq_coe, hx, coe_spanSingleton]

Premises used: FractionalIdeal.coe_spanSingleton, FractionalIdeal.val_eq_coe
-- 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
⊢ (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x

Tactic:
have hx' : (I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x := by
    apply Subtype.coe_injective
    simp only [val_eq_coe, 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
x : K
hx : (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K) = R ∙ x
hx' : (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
⟨Units.mk0 x ?_, ?_⟩

Premises used: Units.mk0, Exists.intro
-- 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
hx' : (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x
refine_1 : x ≠ 0
refine_2 : spanSingleton R⁰ (↑(Units.mk0 x ⋯ : Kˣ) : K) = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
refine ⟨Units.mk0 x ?_, ?_⟩
-- 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
hx' : (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x
x_eq : x = 0
refine_1 : (↑I : FractionalIdeal R⁰ K) = 0
⊢ False

Tactic:
apply Units.ne_zero I

Premises used: Units.ne_zero
-- 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
hx' : (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x
x_eq : x = 0
⊢ (↑I : FractionalIdeal R⁰ K) = 0

Tactic:
simp [hx', x_eq]
-- 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
hx' : (↑I : FractionalIdeal R⁰ K) = spanSingleton R⁰ x
⊢ spanSingleton R⁰ (↑(Units.mk0 x ⋯ : Kˣ) : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
simp [hx']
-- 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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : IsUnit I
rcases : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
⊢ (↑I : Submodule R K).IsPrincipal

Tactic:
rcases hI with ⟨I, rfl⟩

Premises used: rfl
-- 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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
rw :
  Eq.{u_1 + 1} (α := ClassGroup R) ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := ClassGroup R) 1 1
⊢ (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal

Tactic:
rw [← ClassGroup.mk_eq_one_iff, Subsingleton.elim (ClassGroup.mk K I) 1]

Premises used: ClassGroup.mk_eq_one_iff, Subsingleton.elim, OfNat.ofNat, DFunLike.coe, ClassGroup.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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : Ideal R
hI : IsUnit.{u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K)
⊢ Submodule.IsPrincipal.{u_1, u_2} (M := K) (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K)

Tactic:
have hsub :
      ((I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal :=
    ClassGroup.isPrincipal_coeSubmodule_of_isUnit (I := (I : FractionalIdeal R⁰ K)) hI
-- 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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : Ideal R
hI : IsUnit.{u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K)
hsub : Submodule.IsPrincipal.{u_1, u_2} (M := K) (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K)
⊢ Submodule.IsPrincipal (coeSubmodule K I)

Tactic:
simpa using hsub
-- 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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : Ideal R
hI : IsUnit.{u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑I : FractionalIdeal R⁰ K)
hsub : Submodule.IsPrincipal.{u_1, u_2} (M := K) (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K)
⊢ Submodule.IsPrincipal I

Tactic:
exact (IsFractionRing.coeSubmodule_isPrincipal (R := R) (K := K) (I := I)).1
    (by simpa using hsub)

Premises used: Iff.mp, IsFractionRing.coeSubmodule_isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I : Ideal R
hI : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ I
⊢ Eq (α := ClassGroup R)
      ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R)
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) I hI) :
        ClassGroup R)
      (1 : ClassGroup R) ↔
    Submodule.IsPrincipal I

Tactic:
ClassGroup.mk_eq_one_iff.trans (coeSubmodule_isPrincipal R _)

Premises used: ClassGroup.mk_eq_one_iff, Iff.trans, IsFractionRing.coeSubmodule_isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
rw :
  (∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a) ↔
    ∃ (x : R), x ≠ 0 ∧ (↑I : Ideal R) * (↑J : Ideal R) = Ideal.span {x}
⊢ Eq (α := ClassGroup R) ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I : ClassGroup R)
      (((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) J)⁻¹ : ClassGroup R) ↔
    ∃ (x : R), x ≠ 0 ∧ (↑I : Ideal R) * (↑J : Ideal R) = Ideal.span {x}

Tactic:
rw [eq_inv_iff_mul_eq_one, ← map_mul, ClassGroup.mk0_eq_one_iff,
    Submodule.isPrincipal_iff, Submonoid.coe_mul]

Premises used: ClassGroup.mk0_eq_one_iff, eq_inv_iff_mul_eq_one, Submodule.isPrincipal_iff, map_mul, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a) ↔
    ∃ (x : R), x ≠ 0 ∧ (↑I : Ideal R) * (↑J : Ideal R) = Ideal.span {x}

Tactic:
⟨fun ⟨a, ha⟩ ↦ ⟨a, ?_, ha⟩, fun ⟨a, _, ha⟩ ↦ ⟨a, ha⟩⟩

Premises used: HMul.hMul, Exists, _private.0.ClassGroup.mk0_eq_mk0_inv_iff.match_1, Ne, _private.0.ClassGroup.mk0_eq_mk0_inv_iff.match_2, And, And.intro, Iff.intro, Exists.intro, Submodule.span, Ideal.span, Singleton.singleton, OfNat.ofNat, Subtype.val, Eq
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
refine :
  (∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a) → ∀ (a : R) (ha : (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a), a ≠ 0
⊢ (∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a) ↔
    ∃ (x : R), x ≠ 0 ∧ (↑I : Ideal R) * (↑J : Ideal R) = Ideal.span {x}

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a, ?_, ha⟩, fun ⟨a, _, ha⟩ ↦ ⟨a, ha⟩⟩
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
h : ∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
a : R
ha : (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
by_contra! : ∀ (this : a = 0), False
⊢ a ≠ 0

Tactic:
by_contra!
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
h : ∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
a : R
ha : (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
this : a = 0
⊢ (↑I : Ideal R) * (↑J : Ideal R) = ⊥

Tactic:
rw [this, Submodule.span_zero_singleton] at ha

Premises used: Submodule.span_zero_singleton
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
h : ∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
a : R
ha : (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
this : a = 0
ha₁ : (↑I : Ideal R) * (↑J : Ideal R) = ⊥
⊢ a = 0

Tactic:
rw [this, Submodule.span_zero_singleton] at ha

Premises used: Submodule.span_zero_singleton
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
h : ∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
a : R
ha : (↑I : Ideal R) * (↑J : Ideal R) = ⊥
this : a = 0
⊢ False

Tactic:
nonZeroDivisors.coe_ne_zero _ <| J.prop.2 _ ha

Premises used: And.right, Subtype.prop, nonZeroDivisors.coe_ne_zero
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
h : ∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a
a : R
ha : (↑I : Ideal R) * (↑J : Ideal R) = ⊥
this : a = 0
⊢ False

Tactic:
exact nonZeroDivisors.coe_ne_zero _ <| J.prop.2 _ ha

Premises used: And.right, Subtype.prop, nonZeroDivisors.coe_ne_zero
-- 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
inst_5 : IsPrincipalIdealRing R
⊢ ∀ (x : ClassGroup R), Membership.mem (γ := Finset (ClassGroup R)) {1} x

Tactic:
ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)

Premises used: ClassGroup.induction
-- 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
inst_5 : IsPrincipalIdealRing R
refine :
  ∀ (I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    Membership.mem (α := ClassGroup R) (γ := Finset (ClassGroup R)) {1}
      ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
⊢ ∀ (x : ClassGroup R), Membership.mem (γ := Finset (ClassGroup R)) {1} x

Tactic:
refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
-- 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
inst_5 : IsPrincipalIdealRing R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
rw :
  Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)
⊢ Membership.mem (α := ClassGroup R) (γ := Finset (ClassGroup R)) {1}
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)

Tactic:
rw [Finset.mem_singleton]

Premises used: Finset.mem_singleton
-- 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
inst_5 : IsPrincipalIdealRing R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)

Tactic:
ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

Premises used: Iff.mpr, Units.val, ClassGroup.mk_eq_one_iff, FractionalIdeal.isPrincipal
-- 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
inst_5 : IsPrincipalIdealRing R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)

Tactic:
exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

Premises used: Iff.mpr, Units.val, ClassGroup.mk_eq_one_iff, FractionalIdeal.isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
rw : ∃ (x : ClassGroup R), ∀ (y : ClassGroup R), y = x
⊢ Fintype.card.{u_1} (ClassGroup R) = 1

Tactic:
rw [Fintype.card_eq_one_iff]

Premises used: Fintype.card_eq_one_iff
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ∀ (y : ClassGroup R), y = 1
⊢ ∃ (x : ClassGroup R), ∀ (y : ClassGroup R), y = x

Tactic:
use 1
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
⊢ ∀ (y : ClassGroup R), y = 1

Tactic:
ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)

Premises used: ClassGroup.induction
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h :
  ∀ (I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    Eq (α := ClassGroup R)
      ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
      (1 : ClassGroup R)
⊢ ∀ (y : ClassGroup R), y = 1

Tactic:
refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)

Tactic:
ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

Premises used: Iff.mpr, Units.val, ClassGroup.mk_eq_one_iff, FractionalIdeal.isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)

Tactic:
exact ClassGroup.mk_eq_one_iff.mpr (I : FractionalIdeal R⁰ (FractionRing R)).isPrincipal

Premises used: Iff.mpr, Units.val, ClassGroup.mk_eq_one_iff, FractionalIdeal.isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
mp : Fintype.card.{u_1} (ClassGroup R) = 1 → IsPrincipalIdealRing R
mpr : IsPrincipalIdealRing R → Fintype.card.{u_1} (ClassGroup R) = 1
⊢ Fintype.card.{u_1} (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R

Tactic:
constructor
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
h : IsPrincipalIdealRing R
⊢ Fintype.card.{u_1} (ClassGroup R) = 1

Tactic:
card_classGroup_eq_one (R := R)

Premises used: card_classGroup_eq_one
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
h : IsPrincipalIdealRing R
⊢ Fintype.card.{u_1} (ClassGroup R) = 1

Tactic:
convert! card_classGroup_eq_one (R := R)

Premises used: card_classGroup_eq_one
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
mp : (∃ (x : ClassGroup R), ∀ (y : ClassGroup R), y = x) → IsPrincipalIdealRing R
⊢ Fintype.card.{u_1} (ClassGroup R) = 1 → IsPrincipalIdealRing R

Tactic:
rw [Fintype.card_eq_one_iff]

Premises used: Fintype.card_eq_one_iff
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I
⊢ ∀ (J : ClassGroup R), J = 1

Tactic:
have eq_one : ∀ J : ClassGroup R, J = 1 := fun J => (hI J).trans (hI 1).symm
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I
eq_one : ∀ (J : ClassGroup R), J = 1
⊢ IsPrincipalIdealRing R

Tactic:
⟨fun I => ?_⟩

Premises used: IsPrincipalIdealRing.mk
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I
eq_one : ∀ (J : ClassGroup R), J = 1
mp : ∀ (I : Ideal R), Submodule.IsPrincipal I
⊢ IsPrincipalIdealRing R

Tactic:
refine ⟨fun I => ?_⟩
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I_1 : ClassGroup R
hI : ∀ (y : ClassGroup R), y = I_1
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
pos : ∀ (hI : I = ⊥), Submodule.IsPrincipal I
neg : ∀ (hI : ¬I = ⊥), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
by_cases hI : I = ⊥
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I_1 : ClassGroup R
hI_1 : ∀ (y : ClassGroup R), y = I_1
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
pos : Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥
⊢ Submodule.IsPrincipal I

Tactic:
rw [hI]
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I_1 : ClassGroup R
hI_1 : ∀ (y : ClassGroup R), y = I_1
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥

Tactic:
bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I_1 : ClassGroup R
hI_1 : ∀ (y : ClassGroup R), y = I_1
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥

Tactic:
exact bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I_1 : ClassGroup R
hI_1 : ∀ (y : ClassGroup R), y = I_1
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : ¬I = ⊥
⊢ Submodule.IsPrincipal I

Tactic:
(ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _)

Premises used: Iff.mpr, ClassGroup.mk0_eq_one_iff, Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
I_1 : ClassGroup R
hI_1 : ∀ (y : ClassGroup R), y = I_1
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : ¬I = ⊥
⊢ Submodule.IsPrincipal I

Tactic:
exact (ClassGroup.mk0_eq_one_iff (mem_nonZeroDivisors_iff_ne_zero.mpr hI)).mp (eq_one _)

Premises used: Iff.mpr, ClassGroup.mk0_eq_one_iff, Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- 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
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
h :
  ∀ (I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ),
    Membership.mem (γ := Subgroup (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ)
        (Subgroup.map
          (MulEquiv.toMonoidHom
            (Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L)))
          (MonoidHom.range (toPrincipalIdeal R K)))
        I ↔
      Membership.mem (γ := Subgroup (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ)
        (MonoidHom.range (toPrincipalIdeal S L)) I
⊢ Subgroup.map
      (MulEquiv.toMonoidHom
        (Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L)))
      (MonoidHom.range (toPrincipalIdeal R K)) =
    MonoidHom.range (toPrincipalIdeal S L)

Tactic:
ext I
-- 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
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h :
  (∃ (x : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
      (∃ (x_1 : Kˣ), spanSingleton R⁰ (↑x_1 : K) = (↑x : FractionalIdeal R⁰ K)) ∧
        ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
                MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                  (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
            x =
          I) ↔
    ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
⊢ Membership.mem (γ := Subgroup (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ)
      (Subgroup.map
        (MulEquiv.toMonoidHom
          (Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L)))
        (MonoidHom.range (toPrincipalIdeal R K)))
      I ↔
    Membership.mem (γ := Subgroup (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) (MonoidHom.range (toPrincipalIdeal S L))
      I

Tactic:
simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.mem_range,
    toPrincipalIdeal_eq_iff, MonoidHom.coe_coe]

Premises used: MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MonoidHom.mem_range, toPrincipalIdeal_eq_iff, Subgroup.mem_map