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
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
have a : 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: apply Subtype.coe_injective
-- 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
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
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
have hx' : (↑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]
-- 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)ˣ
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)
have refine_1 : x ≠ 0
Tactic: refine ⟨Units.mk0 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.{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
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
have refine_2 : spanSingleton R⁰ (↑(Units.mk0 x sorry : Kˣ) : K) = (↑I : FractionalIdeal R⁰ K)
Tactic: refine ⟨Units.mk0 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.{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
⊢ False
have refine_1 : (↑I : FractionalIdeal R⁰ K) = 0
Tactic: apply Units.ne_zero 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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : IsUnit I
⊢ (↑I : Submodule R K).IsPrincipal
have rcases : ∀ (I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ), (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
Tactic: rcases hI with ⟨I, rfl⟩
Cleared hypotheses: I, hI
-- 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
inst_5 : Subsingleton.{u_1 + 1} (ClassGroup R)
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
have rw : Eq.{u_1 + 1} (α := ClassGroup R) ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)
  (1 : ClassGroup R)
Tactic: rw [← ClassGroup.mk_eq_one_iff, Subsingleton.elim (ClassGroup.mk K I) 1]
-- 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
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)
⊢ (↑(↑I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal
have rw₁ : Eq.{u_1 + 1} (α := ClassGroup R) 1 1
Tactic: rw [← ClassGroup.mk_eq_one_iff, Subsingleton.elim (ClassGroup.mk K I) 1]
-- 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
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 I
have hsub : 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
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ 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}
have rw : (∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a) ↔
  ∃ (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]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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}
have refine : (∃ (a : R), (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a) → ∀ (a : R) (ha : (↑I : Ideal R) * (↑J : Ideal R) = R ∙ a), a ≠ 0
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ ⟨a, ?_, ha⟩, fun ⟨a, _, ha⟩ ↦ ⟨a, ha⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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
⊢ False
have ha₁ : (↑I : Ideal R) * (↑J : Ideal R) = ⊥
Tactic: rw [this, Submodule.span_zero_singleton] at ha
Cleared hypotheses: ha, 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
inst_5 : IsPrincipalIdealRing R
⊢ ∀ (x : ClassGroup R), Membership.mem (γ := Finset (ClassGroup R)) {1} x
have 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)
Tactic: refine ClassGroup.induction (R := R) (FractionRing R) (fun 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
inst_5 : IsPrincipalIdealRing R
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)
have rw : Eq (α := ClassGroup R)
  ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
  (1 : ClassGroup R)
Tactic: rw [Finset.mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
⊢ Fintype.card.{u_1} (ClassGroup R) = 1
have rw : ∃ (x : ClassGroup R), ∀ (y : ClassGroup R), y = x
Tactic: rw [Fintype.card_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
⊢ ∃ (x : ClassGroup R), ∀ (y : ClassGroup R), y = x
have h : ∀ (y : ClassGroup R), y = 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
⊢ ∀ (y : ClassGroup R), y = 1
have 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)
Tactic: refine ClassGroup.induction (R := R) (FractionRing R) (fun I => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
⊢ Fintype.card.{u_1} (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R
have mp : Fintype.card.{u_1} (ClassGroup R) = 1 → IsPrincipalIdealRing R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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
⊢ Fintype.card.{u_1} (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R
have mpr : IsPrincipalIdealRing R → Fintype.card.{u_1} (ClassGroup R) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDedekindDomain R
inst_3 : Fintype (ClassGroup R)
⊢ Fintype.card.{u_1} (ClassGroup R) = 1 → IsPrincipalIdealRing R
have mp : (∃ (x : ClassGroup R), ∀ (y : ClassGroup R), y = x) → IsPrincipalIdealRing R
Tactic: rw [Fintype.card_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (hypothesis)
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
⊢ IsPrincipalIdealRing R
have eq_one : ∀ (J : ClassGroup R), J = 1
Tactic: have eq_one : ∀ J : ClassGroup R, J = 1 := fun J => (hI J).trans (hI 1).symm
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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
have mp : ∀ (I : Ideal R), Submodule.IsPrincipal I
Tactic: refine ⟨fun I => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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
⊢ Submodule.IsPrincipal I
have pos : ∀ (hI : I = ⊥), Submodule.IsPrincipal I
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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
⊢ Submodule.IsPrincipal I
have neg : ∀ (hI : ¬I = ⊥), Submodule.IsPrincipal I
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
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
have pos : Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥
Tactic: rw [hI]
-- 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
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
⊢ 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)
have 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
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
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)ˣ
⊢ 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
have 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)
Tactic: simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.mem_range,
    toPrincipalIdeal_eq_iff, MonoidHom.coe_coe]
-- 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
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)ˣ
⊢ (∃ (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)
have 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) →
  ∀ (u : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (v : Kˣ)
    (huv : spanSingleton R⁰ (↑v : K) = (↑u : FractionalIdeal R⁰ K))
    (hu :
      ((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)ˣ)
          u =
        I),
    ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
Tactic: refine ⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
-- 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
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) →
    ∀ (u : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (v : Kˣ)
      (huv : spanSingleton R⁰ (↑v : K) = (↑u : FractionalIdeal R⁰ K))
      (hu :
        ((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)ˣ)
            u =
          I),
      ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
⊢ (∃ (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)
have h₁ : (∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)) →
  ∀ (u : Lˣ) (hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)),
    ∃ (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
Tactic: refine ⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
-- 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
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
u : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ (↑v : K) = (↑u : FractionalIdeal R⁰ K)
hu :
  ((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)ˣ)
      u =
    I
⊢ ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
have h : spanSingleton S⁰
    (↑(((Units.map (↑(RingEquiv.toRingHom (IsFractionRing.ringEquivOfRingEquiv f)) : K →* L) :
              MonoidHom.{u_2, u_4} Kˣ Lˣ) :
            (a : Kˣ) → Lˣ)
          v) :
      L) =
  (↑I : FractionalIdeal S⁰ L)
Tactic: use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
      (L := L)).toRingHom v
-- 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
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
u : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ (↑v : K) = (↑u : FractionalIdeal R⁰ K)
hu :
  ((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)ˣ)
      u =
    I
⊢ spanSingleton S⁰
      (↑(((Units.map (↑(RingEquiv.toRingHom (IsFractionRing.ringEquivOfRingEquiv f)) : K →* L) :
                MonoidHom.{u_2, u_4} Kˣ Lˣ) :
              (a : Kˣ) → Lˣ)
            v) :
        L) =
    (↑I : FractionalIdeal S⁰ L)
have h : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
  (spanSingleton S⁰
    (↑(((Units.map (↑(RingEquiv.toRingHom (IsFractionRing.ringEquivOfRingEquiv f)) : K →* L) :
              MonoidHom.{u_2, u_4} Kˣ Lˣ) :
            (a : Kˣ) → Lˣ)
          v) :
      L))
  (↑(((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)ˣ)
        u) :
    FractionalIdeal S⁰ L)
Tactic: rw [← hu]