awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ChainOfDivisors (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
⊢ Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) (Associates.mk p)
have h : ∀ (q : Associates M) (hq : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) q)
  (hq' : Associated (Associates.mk p) q),
  Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) (Associates.mk p)
Tactic: obtain ⟨q, hq, hq'⟩ :=
    exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
      (prime_mk.mpr (prime_of_normalized_factor p hp)).irreducible
      (mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : Kˣ
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑((toPrincipalIdeal R K : (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ) x) : FractionalIdeal R⁰ K)
    (spanSingleton R⁰ (↑x : K))
have simp : Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (↑(({
            toFun := fun (x : Kˣ) ↦
              { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := sorry, inv_val := sorry },
            map_one' := sorry, map_mul' := sorry } :
          (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
        x) :
    FractionalIdeal R⁰ K)
  (spanSingleton R⁰ (↑x : K))
Tactic: simp only [toPrincipalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : Kˣ
⊢ (toPrincipalIdeal R K : (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ) x = I ↔
    spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
have simp : ({
          toFun := fun (x : Kˣ) ↦
            { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := sorry, inv_val := sorry },
          map_one' := sorry, map_mul' := sorry } :
        (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
      x =
    I ↔
  spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
Tactic: simp only [toPrincipalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))
      I ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
have simp : (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
  ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
Tactic: simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
have mp : (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) →
  ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
mp :
  (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) →
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
have mpr : (∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)) →
  ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
have mpr : x ≠ 0
Tactic: refine ⟨Units.mk0 x ?_, hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α :=
    Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
    (Quot.mk
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
      I)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I)
have rw : Eq (α :=
  Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
    (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
      (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
  (Quot.mk
    (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
      (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
    I)
  (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
Tactic: rw [ClassGroup.mk_def, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id,
    MonoidHom.id_apply, QuotientGroup.mk'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I J : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ 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
have 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
Tactic: rw [mk_def, mk_def, QuotientGroup.mk'_eq_mk']
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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))
⊢ 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'
have rw : (∃ (x : (FractionRing R)ˣ),
    HMul.hMul (β := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) I
        ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ) x :
          (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
      J) ↔
  ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
Tactic: rw [ClassGroup.mk_eq_mk]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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 : (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'
have 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'
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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'
⊢ (∃ (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'
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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))
⊢ ∃ (x : R) (y : R), x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
have hJ₁ : 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
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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'
⊢ ∃ (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
have 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 sorry))
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
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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
have 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
Tactic: refine ⟨this.unit, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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))ˣ) I
      ((toPrincipalIdeal R (FractionRing R) : (a : (FractionRing R)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          this.unit :
        (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) =
    J
have mpr : spanSingleton R⁰ (↑this.unit : FractionRing R) * (↑I : FractionalIdeal R⁰ (FractionRing R)) =
  (↑J : FractionalIdeal R⁰ (FractionRing R))
Tactic: rw [mul_comm, ← Units.val_inj, Units.val_mul, coe_toPrincipalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing 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}
have 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}
Tactic: rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)),
    ClassGroup.mk_eq_mk_of_coe_ideal hI]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
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}
⊢ 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}
have rw₁ : Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑1 : FractionalIdeal R⁰ (FractionRing R))
  (↑⊤ : FractionalIdeal R⁰ (FractionRing R))
Tactic: rw [← map_one (ClassGroup.mk (R := R) (K := FractionRing R)),
    ClassGroup.mk_eq_mk_of_coe_ideal hI]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑I' : FractionalIdeal R⁰ (FractionRing R))
⊢ (∃ (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}
have 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}
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
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}
⊢ (∃ (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}
have 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}) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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}) ⊤
⊢ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}
have h₁ : Ideal.span {x} * I' = Ideal.span {y}
Tactic: rw [Ideal.mul_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
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}
⊢ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}
have 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}
Tactic: rcases Ideal.mem_span_singleton_mul.mp ((Ideal.span_singleton_le_iff_mem _).mp h.ge) with
      ⟨i, _hi, rfl⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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}
⊢ ∃ (x : R), x ≠ 0 ∧ I' = Ideal.span {x}
have h₁ : I' = Ideal.span {i}
Tactic: rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_mul_right_inj hx] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : (↑I : FractionalIdeal R⁰ (FractionRing R)) = (↑(Ideal.span {x}) : FractionalIdeal R⁰ (FractionRing R))
⊢ HMul.hMul (α := Ideal R) (Ideal.span {1}) (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
have rw : HMul.hMul (α := Ideal R) ⊤ (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
Tactic: rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
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}) ⊤
⊢ HMul.hMul (α := Ideal R) (Ideal.span {1}) (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
have rw₁ : Ideal.span {x} = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
Tactic: rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
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}) ⊤
⊢ HMul.hMul (α := Ideal R) (Ideal.span {1}) (Ideal.span {x}) = HMul.hMul (α := Ideal R) (Ideal.span {x}) ⊤
have rw₂ : Eq (α := Ideal R) (Ideal.span {x}) (Ideal.span {x})
Tactic: rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]