awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))ˣ
⊢ P (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
have 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)
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]
-- 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
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))ˣ
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)
have rw : P
  (↑((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)) :
    (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
Tactic: rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]
-- 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
inst_4 : IsDomain R
⊢ Eq (α := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
    (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
        MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
          (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
    (MonoidHom.range (toPrincipalIdeal R K))
have h : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
  Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
          MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
            (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
          Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
      I ↔
    Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))
      I
Tactic: ext I
-- 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
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
          MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
            (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) :
          Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
      I ↔
    Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))
      I
have h : (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I) ↔
  ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
Tactic: simp only [Subgroup.mem_map, mem_principal_ideals_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
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
have h : (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I) →
  ∃ (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
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
h :
  (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I) →
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ (∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
      (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
        (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            x =
          I) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
have h₁ : (∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)) →
  ∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I
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
inst_4 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ ∃ (x : K),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
      (↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  ((↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: refine ⟨FractionRing.algEquiv R K x, ?_⟩
-- 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
inst_4 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
x : FractionRing R
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
              (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (spanSingleton R⁰ ((FractionRing.algEquiv R K : (a : FractionRing R) → K) x) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (spanSingleton R⁰ ((IsLocalization.map (M := R⁰) (T := R⁰) K (RingHom.id R) sorry : (a : FractionRing R) → K) x) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
-- 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
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I
have h : Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
  (spanSingleton R⁰
      (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
    FractionalIdeal (R := R) R⁰ (FractionRing R))
  ((↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      FractionalIdeal (R := R) R⁰ (FractionRing R)) :
    FractionalIdeal (R := R) R⁰ (FractionRing R))
Tactic: refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
-- 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
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
h :
  Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    ((↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I) :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
⊢ ∃ (x : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    (∃ (x_1 : FractionRing R), spanSingleton R⁰ x_1 = (↑x : FractionalIdeal R⁰ (FractionRing R))) ∧
      (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          x =
        I
have h₁ : (↑((MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
        ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I)) :
    FractionalIdeal R⁰ K) =
  (↑I : FractionalIdeal R⁰ K)
Tactic: refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
-- 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
inst_4 : IsDomain R
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
    (spanSingleton R⁰
        (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
    ((↑((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ K (FractionRing R))) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I) :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) :
      FractionalIdeal (R := R) R⁰ (FractionRing R))
have h : Eq.{u_1 + 1} (α := FractionalIdeal (R := R) R⁰ (FractionRing R))
  (spanSingleton R⁰
      (((AlgEquiv.symm (FractionRing.algEquiv R K) : K ≃ₐ[R] FractionRing R) : (a : K) → FractionRing R) x) :
    FractionalIdeal (R := R) R⁰ (FractionRing R))
  (spanSingleton R⁰
      ((IsLocalization.map (M := R⁰) (T := R⁰) (FractionRing R) (RingHom.id R) sorry : (a : K) → FractionRing R) x) :
    FractionalIdeal (R := R) R⁰ (FractionRing R))
Tactic: simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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
⊢ MulEquiv.{u_1, u_2} (ClassGroup R)
    (HasQuotient.Quotient (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (B :=
      Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K)))
have this : Eq (α := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
  (Subgroup.map (G := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
    (MulEquiv.toMonoidHom (Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K))) :
      MonoidHom.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
    (MonoidHom.range (toPrincipalIdeal R (FractionRing R)) : Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ))
  (MonoidHom.range (toPrincipalIdeal R K))
Tactic: haveI : Subgroup.map
    (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
    (toPrincipalIdeal R (FractionRing R)).range = (toPrincipalIdeal R K).range := by
    ext I
    simp only [Subgroup.mem_map, mem_principal_ideals_iff]
    constructor
    · rintro ⟨I, ⟨x, hx⟩, rfl⟩
      refine ⟨FractionRing.algEquiv R K x, ?_⟩
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
      rfl
    · rintro ⟨x, hx⟩
      refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
      · simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
        rfl
      · simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv,
          RingEquiv.coe_toMulEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_self,
          RingEquiv.refl_apply]
-- 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
inst_4 : IsDomain R
K' : Type u_3
inst_5 : Field K'
inst_6 : Algebra R K'
inst_7 : IsFractionRing R K'
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Eq (α :=
    HasQuotient.Quotient (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ (B :=
      Subgroup (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) (MonoidHom.range (toPrincipalIdeal R K')))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K')) :
          (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ K')ˣ ⧸ (toPrincipalIdeal R K').range)
        ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K')ˣ)
          (((Units.map
                  (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                    FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
                MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                  (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
              (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I)) :
      HasQuotient.Quotient (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) (MonoidHom.range (toPrincipalIdeal R K')))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K')) :
          (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ K')ˣ ⧸ (toPrincipalIdeal R K').range)
        (((Units.mapEquiv (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K ≃* FractionalIdeal R⁰ K') :
              MulEquiv.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K')ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ (B :=
        Subgroup (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) (MonoidHom.range (toPrincipalIdeal R K')))
have h : Eq.{u_3 + 1} (α := (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
  ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) :
        (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K')ˣ)
      (((Units.map
              (↑(canonicalEquiv R⁰ K (FractionRing R)) : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
            MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
              (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
          (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        I) :
    (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
  (((Units.mapEquiv (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K ≃* FractionalIdeal R⁰ K') :
          MulEquiv.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
            (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K')ˣ)
      I :
    (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
Tactic: congr
-- 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
inst_4 : IsDomain R
K' : Type u_3
inst_5 : Field K'
inst_6 : Algebra R K'
inst_7 : IsFractionRing R K'
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Eq.{u_3 + 1} (α := (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
    ((Units.mapEquiv (RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K')) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K')ˣ)
        (((Units.map
                (↑(canonicalEquiv R⁰ K (FractionRing R)) :
                  FractionalIdeal R⁰ K →* FractionalIdeal R⁰ (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
    (((Units.mapEquiv (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K ≃* FractionalIdeal R⁰ K') :
            MulEquiv.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
              (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ) :
          (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K')ˣ)
        I :
      (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
have h : Eq.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')
  ((RingEquiv.toMulEquiv (canonicalEquiv R⁰ (FractionRing R) K') :
        (a : FractionalIdeal R⁰ (FractionRing R)) → FractionalIdeal R⁰ K')
      ((((↑(canonicalEquiv R⁰ K (FractionRing R)) :
              MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
                (FractionalIdeal (R := R) R⁰ (FractionRing R))) :
            MonoidHom.{u_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
              (FractionalIdeal (R := R) R⁰ (FractionRing R))) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ (FractionRing R))
        (↑I : FractionalIdeal R⁰ K)) :
    FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')
  ((((↑(canonicalEquiv R⁰ K K') :
            MulEquiv.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
              (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')) :
          MulEquiv.{u_2, u_3} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')) :
        (a : FractionalIdeal R⁰ K) → FractionalIdeal R⁰ K')
      (↑I : FractionalIdeal R⁰ K) :
    FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')
Tactic: rw [← Units.val_inj, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]