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
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_1 + 1} (α := ClassGroup R)
    ((mk K' : (a : (FractionalIdeal R⁰ K')ˣ) → ClassGroup R)
        (((Units.map (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K') :
              MonoidHom.{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) :
      ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)
have rw : Eq (α := ClassGroup R)
  ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R (FractionRing R))) :
        (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) →
          (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
      (((Units.map
              (↑(canonicalEquiv R⁰ K' (FractionRing R)) :
                FractionalIdeal R⁰ K' →* FractionalIdeal R⁰ (FractionRing R)) :
            MonoidHom.{u_3, u_1} (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ
              (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
          (a : (FractionalIdeal R⁰ K')ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        (((Units.map (↑(canonicalEquiv R⁰ K K') : FractionalIdeal R⁰ K →* FractionalIdeal R⁰ K') :
              MonoidHom.{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 (R := R) R⁰ (FractionRing R))ˣ (B :=
      Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))
  ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : ClassGroup R)
Tactic: rw [ClassGroup.mk_def, ClassGroup.mk_def, ← MonoidHom.comp_apply (Units.map _),
      ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans,
      FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]
-- 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 : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I : ClassGroup R)
have rw : Eq.{u_1 + 1} (α := ClassGroup R)
  ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
      ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
    ClassGroup R)
  ((MonoidHom.comp (N := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) (mk (FractionRing R))
          (FractionalIdeal.mk0 (FractionRing R)) :
        (a : ↥(Ideal R)⁰) → ClassGroup R)
      I :
    ClassGroup R)
Tactic: rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
    FractionalIdeal.map_canonicalEquiv_mk0]
-- 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 : IsDedekindDomain R
I : ↥(Ideal R)⁰
rw :
  Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((MonoidHom.comp (N := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) (mk (FractionRing R))
            (FractionalIdeal.mk0 (FractionRing R)) :
          (a : ↥(Ideal R)⁰) → ClassGroup R)
        I :
      ClassGroup R)
⊢ Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I : ClassGroup R)
have rw₁ : Eq (α := ClassGroup R)
  ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
      ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
    ClassGroup R)
  ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
      (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
          (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        I) :
    ClassGroup R)
Tactic: rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
    FractionalIdeal.map_canonicalEquiv_mk0]
-- 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 : IsDedekindDomain R
I : ↥(Ideal R)⁰
rw :
  Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((MonoidHom.comp (N := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) (mk (FractionRing R))
            (FractionalIdeal.mk0 (FractionRing R)) :
          (a : ↥(Ideal R)⁰) → ClassGroup R)
        I :
      ClassGroup R)
rw₁ :
  Eq (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      ClassGroup R)
⊢ Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I : ClassGroup R)
have rw₂ : Eq.{u_1 + 1} (α := ClassGroup R)
  ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
      (((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))ˣ)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I)) :
    ClassGroup R)
  ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
      (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
          (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        I) :
    ClassGroup R)
Tactic: rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
    FractionalIdeal.map_canonicalEquiv_mk0]
-- 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 : IsDedekindDomain R
I : ↥(Ideal R)⁰
rw :
  Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((MonoidHom.comp (N := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) (mk (FractionRing R))
            (FractionalIdeal.mk0 (FractionRing R)) :
          (a : ↥(Ideal R)⁰) → ClassGroup R)
        I :
      ClassGroup R)
rw₁ :
  Eq (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      ClassGroup R)
rw₂ :
  Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((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))ˣ)
          ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I)) :
      ClassGroup R)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      ClassGroup R)
⊢ Eq.{u_1 + 1} (α := ClassGroup R)
    ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      ClassGroup R)
    ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I : ClassGroup R)
have rw₃ : Eq (α := ClassGroup R)
  ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
      ((FractionalIdeal.mk0 (FractionRing R) : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ) I) :
    ClassGroup R)
  ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R)
      (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
          (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        I) :
    ClassGroup R)
Tactic: rw [ClassGroup.mk0, MonoidHom.comp_apply, ← ClassGroup.mk_canonicalEquiv K (FractionRing R),
    FractionalIdeal.map_canonicalEquiv_mk0]
-- 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 : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ Eq.{u_2 + 1} (α :=
    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)))
    ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I) :
      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)))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)) :
          (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      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 rw : Eq (α :=
  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)))
  ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
      (((Units.mapEquiv
              (↑(canonicalEquiv R⁰ (FractionRing R) K) : FractionalIdeal R⁰ (FractionRing R) ≃* FractionalIdeal R⁰ K) :
            MulEquiv.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
              (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) :
          (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
        (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I)) :
    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)))
  ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
      ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
    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)))
Tactic: rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]
-- 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 : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ Eq (α :=
    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)))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)) :
          (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        (((Units.mapEquiv
                (↑(canonicalEquiv R⁰ (FractionRing R) K) :
                  FractionalIdeal R⁰ (FractionRing R) ≃* FractionalIdeal R⁰ K) :
              MulEquiv.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
                (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) :
            (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
          (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
              (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
            I)) :
      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)))
    ((QuotientGroup.mk' (MonoidHom.range (toPrincipalIdeal R K)) :
          (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      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 h : Eq.{u_2 + 1} (α := (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
  (((Units.mapEquiv
            (↑(canonicalEquiv R⁰ (FractionRing R) K) : FractionalIdeal R⁰ (FractionRing R) ≃* FractionalIdeal R⁰ K) :
          MulEquiv.{u_1, u_2} (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
            (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) :
        (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → (FractionalIdeal R⁰ K)ˣ)
      (((FractionalIdeal.mk0 (FractionRing R) : ↥(Ideal R)⁰ →* (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
          (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
        I) :
    (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
  ((FractionalIdeal.mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I :
    (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
Tactic: congr 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 : 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 : K) (_ : x ≠ 0),
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
have refine : Eq.{u_2 + 1} (α :=
    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)))
    ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I) :
      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)))
    ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
        ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) J) :
      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))) ↔
  ∃ (x : K) (_ : x ≠ 0),
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
        (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
      (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
Tactic: refine (ClassGroup.equiv K).injective.eq_iff.symm.trans ?_
-- 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 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ Eq.{u_2 + 1} (α :=
      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)))
      ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
          ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) I) :
        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)))
      ((equiv K : (a : ClassGroup R) → (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range)
          ((mk0 : (a : ↥(Ideal R)⁰) → ClassGroup R) J) :
        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))) ↔
    ∃ (x : K) (_ : x ≠ 0),
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
have simp : (∃ (z : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    (∃ (x : K), spanSingleton R⁰ x = (↑z : FractionalIdeal R⁰ K)) ∧
      (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑z : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)) ↔
  ∃ (x : K),
    x ≠ 0 ∧
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
Tactic: simp only [ClassGroup.equiv_mk0, QuotientGroup.mk'_eq_mk', mem_principal_ideals_iff,
    Units.ext_iff, Units.val_mul, FractionalIdeal.coe_mk0, exists_prop]
-- 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 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ (z : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
      (∃ (x : K), spanSingleton R⁰ x = (↑z : FractionalIdeal R⁰ K)) ∧
        (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑z : FractionalIdeal R⁰ K) =
          (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)) ↔
    ∃ (x : K),
      x ≠ 0 ∧
        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
            (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
          (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
have mp : (∃ (z : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    (∃ (x : K), spanSingleton R⁰ x = (↑z : FractionalIdeal R⁰ K)) ∧
      (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑z : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)) →
  ∃ (x : K),
    x ≠ 0 ∧
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : 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
inst_5 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
mp :
  (∃ (z : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
      (∃ (x : K), spanSingleton R⁰ x = (↑z : FractionalIdeal R⁰ K)) ∧
        (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑z : FractionalIdeal R⁰ K) =
          (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)) →
    ∃ (x : K),
      x ≠ 0 ∧
        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
            (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
          (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
⊢ (∃ (z : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
      (∃ (x : K), spanSingleton R⁰ x = (↑z : FractionalIdeal R⁰ K)) ∧
        (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑z : FractionalIdeal R⁰ K) =
          (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)) ↔
    ∃ (x : K),
      x ≠ 0 ∧
        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
            (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
          (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
have mpr : (∃ (x : K),
    x ≠ 0 ∧
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)) →
  ∃ (z : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    (∃ (x : K), spanSingleton R⁰ x = (↑z : FractionalIdeal R⁰ K)) ∧
      (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑z : FractionalIdeal R⁰ K) = (↑(↑J : Ideal R) : 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
inst_5 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
X : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
hx : (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑X : FractionalIdeal R⁰ K) = (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
x : K
hX : spanSingleton R⁰ x = (↑X : FractionalIdeal R⁰ K)
⊢ ∃ (x : K),
    x ≠ 0 ∧
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
have mp : x ≠ 0
Tactic: refine ⟨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
inst_5 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
X : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
hx : (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) * (↑X : FractionalIdeal R⁰ K) = (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
x : K
hX : spanSingleton R⁰ x = (↑X : FractionalIdeal R⁰ K)
mp : x ≠ 0
⊢ ∃ (x : K),
    x ≠ 0 ∧
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
          (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
        (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
have mp₁ : HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ x)
    (↑(↑I : Ideal R) : FractionalIdeal R⁰ K) =
  (↑(↑J : Ideal R) : FractionalIdeal R⁰ K)
Tactic: refine ⟨x, ?_, ?_⟩