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
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)

Tactic:
⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩

Premises used: Units.val, FractionalIdeal.spanSingleton, nonZeroDivisors, Exists, Units.mapEquiv, And, Iff.intro, _private.0.ClassGroup.mk_eq_one_iff.match_2, Eq, MulEquivClass.toMulEquiv, DFunLike.coe, _private.0.FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal.match_1, FractionalIdeal.ringEquivOfRingEquiv
-- 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
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)
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
⊢ (∃ (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:
refine ⟨fun ⟨u, ⟨v, huv⟩, hu⟩ ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
-- 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
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_1 :
  ∃ (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
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)
⊢ ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)

Tactic:
use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
      (L := L)).toRingHom v

Premises used: DFunLike.coe, Units.map
-- 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
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_1 :
  ∃ (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
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)
⊢ 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:
rw [← hu]
-- 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
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_1 :
  ∃ (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
h :
  Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (((ringEquivOfRingEquiv K L f :
            RingEquiv.{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)
        (spanSingleton R⁰ (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
⊢ 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:
simp only [RingEquiv.toRingHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe,
      Units.coe_mapEquiv, ← huv, RingEquiv.coe_toMulEquiv]

Premises used: RingEquiv.coe_toMulEquiv, Units.coe_map, RingHom.coe_coe, MonoidHom.coe_coe, RingEquiv.toRingHom_eq_coe, 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
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_1 :
  ∃ (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
h h₁ :
  Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
⊢ Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (((ringEquivOfRingEquiv K L f :
            RingEquiv.{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)
        (spanSingleton R⁰ (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)

Tactic:
rw [FractionalIdeal.ringEquivOfRingEquiv_spanSingleton]

Premises used: FractionalIdeal.ringEquivOfRingEquiv_spanSingleton
-- 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
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_1 : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
h :
  (∃ (x : Kˣ),
      Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
        (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
                (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
              I) :
          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)ˣ)
        ((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) =
      I
⊢ ∃ (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:
use Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv _ _ f).symm.toMulEquiv I

Premises used: Units.mapEquiv, DFunLike.coe
-- 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
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 : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ 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)ˣ)
      ((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
          (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I) =
    I

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
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_1 : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
h :
  ∃ (x : Kˣ),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
      (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
              (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)
⊢ (∃ (x : Kˣ),
      Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
        (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
                (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
              I) :
          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)ˣ)
        ((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) =
      I

Tactic:
refine ⟨?_, by simp [← 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
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_1 : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
h :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰
      (↑(((Units.map (↑(RingEquiv.toRingHom (RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f))) : L →* K) :
                MonoidHom.{u_4, u_2} Lˣ Kˣ) :
              (a : Lˣ) → Kˣ)
            u) :
        K))
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) :
      FractionalIdeal R⁰ K)
⊢ ∃ (x : Kˣ),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
      (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
              (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)

Tactic:
use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
        (L := L)).symm.toRingHom u

Premises used: DFunLike.coe, Units.map
-- 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
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_1 : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
h :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((IsFractionRing.ringEquivOfRingEquiv f.symm : (a : L) → K) (↑u : L)) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
            MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰
      (↑(((Units.map (↑(RingEquiv.toRingHom (RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f))) : L →* K) :
                MonoidHom.{u_4, u_2} Lˣ Kˣ) :
              (a : Lˣ) → Kˣ)
            u) :
        K))
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) :
      FractionalIdeal R⁰ K)

Tactic:
simp only [IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toRingHom_eq_coe,
        Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.toMulEquiv_eq_coe,
        RingEquiv.coe_toMulEquiv_symm, Units.coe_mapEquiv]

Premises used: Units.coe_map, RingHom.coe_coe, MonoidHom.coe_coe, IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toMulEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toMulEquiv_symm, 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
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_1 : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
h :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((RingEquiv.symm (ringEquivOfRingEquiv K L f) :
            RingEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
              (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
            MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((IsFractionRing.ringEquivOfRingEquiv f.symm : (a : L) → K) (↑u : L)) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
            MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton,
        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]

Premises used: FractionalIdeal.ringEquivOfRingEquiv_symm_eq, FractionalIdeal.ringEquivOfRingEquiv_spanSingleton