awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
h :
  emultiplicity (α := Associates M) (Associates.mk p) (Associates.mk m) =
    emultiplicity (α := Associates N)
      (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
              (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦
              Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
              ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
        Associates N)
      (Associates.mk n)
⊢ emultiplicity (α := Associates M) (Associates.mk p) (Associates.mk m) =
    emultiplicity (α := Associates N)
      (Associates.mk
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
              (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
                ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                  ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
                ⋯)) :
          N))
      (Associates.mk n)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
⊢ emultiplicity (α := Associates M) (Associates.mk p) (Associates.mk m) =
    emultiplicity (α := Associates N)
      (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
              (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦
              Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
              ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
        Associates N)
      (Associates.mk n)

Tactic:
emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso (mk_ne_zero.mpr hn) ?_
      (mkFactorOrderIsoOfFactorDvdEquiv hd)

Premises used: Iff.mpr, emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso, Associates.mk_ne_zero, mkFactorOrderIsoOfFactorDvdEquiv
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
h : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) (Associates.mk p)
⊢ emultiplicity (α := Associates M) (Associates.mk p) (Associates.mk m) =
    emultiplicity (α := Associates N)
      (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
              (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
            (Subtype.mk (p := fun (x : Associates M) ↦
              Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
              ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
        Associates N)
      (Associates.mk n)

Tactic:
refine
    emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso (mk_ne_zero.mpr hn) ?_
      (mkFactorOrderIsoOfFactorDvdEquiv hd)

Premises used: Iff.mpr, emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso, Associates.mk_ne_zero, mkFactorOrderIsoOfFactorDvdEquiv
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
h :
  ∀ (q : Associates M) (hq : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) q)
    (hq' : Associated (Associates.mk p) q),
    Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) (Associates.mk p)
⊢ Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) (Associates.mk p)

Tactic:
obtain ⟨q, hq, hq'⟩ :=
    exists_mem_normalizedFactors_of_dvd (mk_ne_zero.mpr hm)
      (prime_mk.mpr (prime_of_normalized_factor p hp)).irreducible
      (mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp))

Premises used: Prime.irreducible, Iff.mpr, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd, UniqueFactorizationMonoid.prime_of_normalized_factor, Associates.prime_mk, Associates.mk_le_mk_of_dvd, Associates.mk_ne_zero
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
N : Type u_2
inst_2 : CommMonoidWithZero N
inst_3 : Subsingleton.{u_1 + 1} Mˣ
inst_4 : Subsingleton.{u_2 + 1} Nˣ
inst_5 : UniqueFactorizationMonoid M
inst_6 : UniqueFactorizationMonoid N
m p : M
n : N
hm : m ≠ 0
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : Equiv.{max 1 (u_1 + 1), max 1 (u_2 + 1)} { l : M // l ∣ m } { l : N // l ∣ n }
hd :
  ∀ (l l' : { l : M // l ∣ m }),
    Dvd.dvd.{u_2} (α := N) (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l) : N)
        (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n }) l') : N) ↔
      (↑l : M) ∣ (↑l' : M)
this :
  Eq.{u_2 + 1} (α := Associates N)
    (Associates.mk
      (↑((d : (a : { l : M // l ∣ m }) → { l : N // l ∣ n })
            (Subtype.mk (p := fun (l : M) ↦ l ∣ m)
              ((associatesEquivOfUniqueUnits : (a : Associates M) → M)
                ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p : Associates M))
              ⋯)) :
        N))
    (↑((mkFactorOrderIsoOfFactorDvdEquiv hd :
            (a : (↑(Set.Iic (Associates.mk m)) : Type u_1)) → (↑(Set.Iic (Associates.mk n)) : Type u_2))
          (Subtype.mk (p := fun (x : Associates M) ↦
            Membership.mem (γ := Set (Associates M)) (Set.Iic (Associates.mk m)) x)
            ((MulEquiv.symm associatesEquivOfUniqueUnits : (a : M) → Associates M) p) ⋯)) :
      Associates N)
q : Associates M
hq : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) q
hq' : Associated (Associates.mk p) q
h h₁ h₂ h₃ : Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) q
⊢ Membership.mem (γ := Multiset (Associates M)) (normalizedFactors (Associates.mk m)) (Associates.mk p)

Tactic:
rwa [associated_iff_eq.mp hq']

Premises used: associated_iff_eq, Iff.mp
-- 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
x : Kˣ
⊢ HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K)) (spanSingleton R⁰ (↑x : K)⁻¹) =
    1

Tactic:
simp only [spanSingleton_one, Units.mul_inv', spanSingleton_mul_spanSingleton]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, Units.mul_inv', FractionalIdeal.spanSingleton_one
-- 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
x : Kˣ
⊢ HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K)⁻¹) (spanSingleton R⁰ (↑x : K)) =
    1

Tactic:
simp only [spanSingleton_one, Units.inv_mul', spanSingleton_mul_spanSingleton]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, FractionalIdeal.spanSingleton_one, Units.inv_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
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑{ val := spanSingleton R⁰ (↑1 : K), inv := spanSingleton R⁰ (↑1 : K)⁻¹, val_inv := ⋯, inv_val := ⋯ :
          (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ } :
      FractionalIdeal R⁰ K)
    (↑1 : FractionalIdeal R⁰ K)

Tactic:
simp only [spanSingleton_one, Units.val_one]

Premises used: Units.val_one, FractionalIdeal.spanSingleton_one
-- 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
x y : Kˣ
⊢ (↑{ val := spanSingleton R⁰ (↑(x * y) : K), inv := spanSingleton R⁰ (↑(x * y) : K)⁻¹, val_inv := ⋯, inv_val := ⋯ :
          (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ } :
      FractionalIdeal R⁰ K) =
    (↑(HMul.hMul (α := (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ)
          { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := ⋯, inv_val := ⋯ :
            (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ }
          { val := spanSingleton R⁰ (↑y : K), inv := spanSingleton R⁰ (↑y : K)⁻¹, val_inv := ⋯, inv_val := ⋯ :
            (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ }) :
      FractionalIdeal R⁰ K)

Tactic:
simp only [Units.val_mul, spanSingleton_mul_spanSingleton]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, 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
x : Kˣ
simp :
  Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑(({
              toFun := fun (x : Kˣ) ↦
                { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := ⋯, inv_val := ⋯ },
              map_one' := ⋯, map_mul' := ⋯ } :
            (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
          x) :
      FractionalIdeal R⁰ K)
    (spanSingleton R⁰ (↑x : K))
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑((toPrincipalIdeal R K : (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ) x) : FractionalIdeal R⁰ K)
    (spanSingleton R⁰ (↑x : K))

Tactic:
simp only [toPrincipalIdeal]

Premises used: toPrincipalIdeal
-- 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
x : Kˣ
⊢ Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (↑(({
              toFun := fun (x : Kˣ) ↦
                { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := ⋯, inv_val := ⋯ },
              map_one' := ⋯, map_mul' := ⋯ } :
            (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
          x) :
      FractionalIdeal R⁰ K)
    (spanSingleton R⁰ (↑x : K))

Tactic:
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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : Kˣ
simp :
  ({
            toFun := fun (x : Kˣ) ↦
              { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := ⋯, inv_val := ⋯ },
            map_one' := ⋯, map_mul' := ⋯ } :
          (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
        x =
      I ↔
    spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ (toPrincipalIdeal R K : (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ) x = I ↔
    spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
simp only [toPrincipalIdeal]

Premises used: toPrincipalIdeal
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : Kˣ
⊢ ({
            toFun := fun (x : Kˣ) ↦
              { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := ⋯, inv_val := ⋯ },
            map_one' := ⋯, map_mul' := ⋯ } :
          (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
        x =
      I ↔
    spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
Units.ext_iff

Premises used: Units.ext_iff
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : Kˣ
⊢ ({
            toFun := fun (x : Kˣ) ↦
              { val := spanSingleton R⁰ (↑x : K), inv := spanSingleton R⁰ (↑x : K)⁻¹, val_inv := ⋯, inv_val := ⋯ },
            map_one' := ⋯, map_mul' := ⋯ } :
          (a : Kˣ) → (FractionalIdeal R⁰ K)ˣ)
        x =
      I ↔
    spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
exact Units.ext_iff

Premises used: Units.ext_iff
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
simp :
  (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ Membership.mem (γ := Subgroup (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))
      I ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)

Tactic:
simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]

Premises used: MonoidHom.mem_range, toPrincipalIdeal_eq_iff
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
mp :
  (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) →
    ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
mpr :
  (∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)) →
    ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ (∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)) ↔
    ∃ (x : K), spanSingleton R⁰ x = (↑I : 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : Kˣ
hx : spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)

Tactic:
⟨x, hx⟩

Premises used: Units.val, 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : Kˣ
hx : spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : K), spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)

Tactic:
exact ⟨x, hx⟩
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
⟨Units.mk0 x ?_, hx⟩

Premises used: Units.mk0, 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
x : K
hx : spanSingleton R⁰ x = (↑I : FractionalIdeal R⁰ K)
mpr : x ≠ 0
⊢ ∃ (x : Kˣ), spanSingleton R⁰ (↑x : K) = (↑I : FractionalIdeal R⁰ K)

Tactic:
refine ⟨Units.mk0 x ?_, hx⟩
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
hx : spanSingleton R⁰ 0 = (↑I : FractionalIdeal R⁰ K)
⊢ False

Tactic:
simp [I.ne_zero.symm] at hx

Premises used: Units.ne_zero, Ne.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
⊢ Subgroup.Normal (G := (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ) (MonoidHom.range (toPrincipalIdeal R K))

Tactic:
Subgroup.normal_of_isMulCommutative _

Premises used: Subgroup.normal_of_isMulCommutative
-- 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
I : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
⊢ Eq.{u_1 + 1} (α := ClassGroup R) ((mk K : (a : (FractionalIdeal R⁰ K)ˣ) → ClassGroup R) I : 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_2, u_1} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal R⁰ (FractionRing R))ˣ)
          I) :
      HasQuotient.Quotient (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ (B :=
        Subgroup (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
        (MonoidHom.range (toPrincipalIdeal R (FractionRing R))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
rw :
  Eq (α :=
    Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
    (Quot.mk
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
      I)
    (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
⊢ Eq (α :=
    Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
    (Quot.mk
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
      I)
    ((mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I)

Tactic:
rw [ClassGroup.mk_def, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id,
    MonoidHom.id_apply, QuotientGroup.mk'_apply]

Premises used: QuotientGroup.mk'_apply, Units.map_id, MonoidHom.id_apply, FractionalIdeal.canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, ClassGroup.mk_def
-- Module: Mathlib.RingTheory.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α :=
    Quot (α := (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ)
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop))
    (Quot.mk
      (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range) :
        (FractionalIdeal R⁰ (FractionRing R))ˣ → (FractionalIdeal R⁰ (FractionRing R))ˣ → Prop)
      I)
    (↑I : (FractionalIdeal R⁰ (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)

Tactic:
rfl