awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
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)ˣ
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')
⊢ 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:
rw [← Units.val_inj, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]

Premises used: Units.coe_map, Units.val_inj, Units.coe_mapEquiv
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
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')
    ((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:
FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _

Premises used: FractionalIdeal.canonicalEquiv_canonicalEquiv
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
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')
    ((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:
exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _

Premises used: FractionalIdeal.canonicalEquiv_canonicalEquiv
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
⊢ Eq.{u_2 + 1} (α := (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
    (Units.mk0 (↑(↑1 : Ideal R) : FractionalIdeal R⁰ K) ⋯ : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
x y : ↥(Ideal R)⁰
⊢ Units.mk0 (↑(↑(x * y) : Ideal R) : FractionalIdeal R⁰ K) ⋯ =
    HMul.hMul (α := (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (β := (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (Units.mk0 (↑(↑x : Ideal R) : FractionalIdeal R⁰ K) ⋯ : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
      (Units.mk0 (↑(↑y : Ideal R) : FractionalIdeal R⁰ K) ⋯)

Tactic:
simp
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑((mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) : FractionalIdeal R⁰ K)
    (↑(↑I : Ideal R) : FractionalIdeal R⁰ K)

Tactic:
rfl

Premises used: FractionalIdeal.coeIdeal, rfl
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
K' : Type u_3
inst_6 : Field K'
inst_7 : Algebra R K'
inst_8 : IsFractionRing R K'
I : ↥(Ideal R)⁰
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')
    (((canonicalEquiv R⁰ K K' :
          RingEquiv.{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')
      (↑((mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) : FractionalIdeal R⁰ K))
    (↑((mk0 K' : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K')ˣ) I) : FractionalIdeal R⁰ K')

Tactic:
simp only [FractionalIdeal.coe_mk0, FractionalIdeal.canonicalEquiv_coeIdeal]

Premises used: FractionalIdeal.canonicalEquiv_coeIdeal, FractionalIdeal.coe_mk0
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
K' : Type u_3
inst_6 : Field K'
inst_7 : Algebra R K'
inst_8 : IsFractionRing R K'
I : ↥(Ideal R)⁰
⊢ Eq.{u_3 + 1} (α := (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
    (((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')ˣ)
        ((mk0 K : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K)ˣ) I) :
      (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)
    ((mk0 K' : (a : ↥(Ideal R)⁰) → (FractionalIdeal R⁰ K')ˣ) I : (FractionalIdeal.{u_1, u_3} (R := R) R⁰ K')ˣ)

Tactic:
Units.ext (FractionalIdeal.canonicalEquiv_mk0 K K' I)

Premises used: FractionalIdeal.canonicalEquiv_mk0, Units.ext
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
I : ↥(Ideal R)⁰
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)))
⊢ 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)))

Tactic:
rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]

Premises used: ClassGroup.mk0, ClassGroup.equiv_mk, MonoidHom.comp_apply
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
I : ↥(Ideal R)⁰
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)ˣ)
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ 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:
simp [← Units.val_inj]

Premises used: Units.val_inj
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : 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)

Tactic:
(ClassGroup.equiv K).injective.eq_iff.symm.trans ?_

Premises used: Function.Injective.eq_iff, Iff.trans, ClassGroup.equiv, MulEquiv.injective, Iff.symm
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
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)
⊢ 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)

Tactic:
refine (ClassGroup.equiv K).injective.eq_iff.symm.trans ?_

Premises used: Function.Injective.eq_iff, Iff.trans, ClassGroup.equiv, MulEquiv.injective, Iff.symm
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : IsDedekindDomain R
I J : ↥(Ideal R)⁰
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)
⊢ 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:
simp only [ClassGroup.equiv_mk0, QuotientGroup.mk'_eq_mk', mem_principal_ideals_iff,
    Units.ext_iff, Units.val_mul, FractionalIdeal.coe_mk0, exists_prop]

Premises used: Units.ext_iff, mem_principal_ideals_iff, QuotientGroup.mk'_eq_mk', exists_prop, ClassGroup.equiv_mk0, FractionalIdeal.coe_mk0, Units.val_mul
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : 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)
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)
⊢ (∃ (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
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : 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)

Tactic:
⟨x, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
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
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)
⊢ ∃ (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 ⟨x, ?_, ?_⟩