awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsReduced R
inst_3 : IsLocalRing R
⊢ IsField R

Tactic:
(IsArtinianRing.equivPi R).toRingEquiv.trans (RingEquiv.piUnique _) |>.toMulEquiv.isField
    (Ideal.Quotient.field _).toIsField

Premises used: RingEquiv.toMulEquiv, Field.toIsField, RingEquiv.piUnique, IsArtinianRing.equivPi, AlgEquiv.toRingEquiv, MulEquiv.isField, RingEquiv.trans
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r' : L
obtain : ∀ (r₁ : R) (s : ↥S), ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
⊢ ∃ (a : R), (algebraMap R L : (a : R) → L) a = r'

Tactic:
obtain ⟨r₁, s, rfl⟩ := IsLocalization.exists_mk'_eq S r'

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
rsuffices :
  ∀ (r₂ : R) (h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂),
    ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
rsuffices₁ : ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
⊢ ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s

Tactic:
rsuffices ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r

Premises used: IsLocalization.mk', OfNat.ofNat
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂
rw :
  (algebraMap R L : (a : R) → L) (r₁ * r₂) =
    HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
rw₁ :
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L) =
    HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
rw₂ rw₃ :
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L)
⊢ (algebraMap R L : (a : R) → L) (r₁ * r₂) = IsLocalization.mk' L r₁ s

Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]

Premises used: IsLocalization.mk'_eq_mul_mk'_one, map_mul
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂
⊢ ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s

Tactic:
exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
obtain :
  ∀ (n : ℕ) (r : R) (hr : (↑s : R) ^ n.succ • r = HSMul.hSMul (β := R) ((↑s : R) ^ n) 1),
    ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
⊢ ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r

Tactic:
obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)

Premises used: IsArtinian.exists_pow_succ_smul_dvd, OfNat.ofNat, Subtype.val
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : (↑s : R) ^ n.succ • r = HSMul.hSMul (β := R) ((↑s : R) ^ n) 1
h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
⊢ ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r

Tactic:
use r
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : (↑s : R) ^ n.succ • r = HSMul.hSMul (β := R) ((↑s : R) ^ n) 1
⊢ (↑s : R) ^ n * ((↑s : R) * r) = (↑s : R) ^ n * 1

Tactic:
rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr

Premises used: pow_succ, mul_assoc, smul_eq_mul
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : (↑s : R) ^ n * ((↑s : R) * r) = (↑s : R) ^ n * 1
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * ((↑s : R) * r)) : L)
    ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * 1) : L)

Tactic:
apply_fun algebraMap R L at hr

Premises used: Algebra.algebraMap
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr :
  Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * ((↑s : R) * r)) : L)
    ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * 1) : L)
⊢ HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n) : L)
      (HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) (↑s : R) : L)
        ((algebraMap R L : (a : R) → L) r : L)) =
    HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n) : L)
      ((algebraMap R L : (a : R) → L) 1 : L)

Tactic:
simp only [map_mul] at hr

Premises used: map_mul
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr :
  HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n) : L)
      (HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) (↑s : R) : L)
        ((algebraMap R L : (a : R) → L) r : L)) =
    HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n) : L)
      ((algebraMap R L : (a : R) → L) 1 : L)
h : IsLocalization.mk' L 1 s = IsLocalization.mk' (M := S) L r 1
h₁ :
  Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) (HMul.hMul (α := R) (↑1 : R) 1) : L)
    ((algebraMap R L : (a : R) → L) ((↑s : R) * r) : L)
h₂ :
  Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) (↑1 : R) : L)
    ((algebraMap R L : (a : R) → L) ((↑s : R) * r) : L)
h₃ : Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) 1 : L) ((algebraMap R L : (a : R) → L) ((↑s : R) * r) : L)
h₄ :
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) (↑s : R) : L) ((algebraMap R L : (a : R) → L) r : L) =
    (algebraMap R L : (a : R) → L) ((↑s : R) * r)
h₅ h₆ :
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) (↑s : R) : L) ((algebraMap R L : (a : R) → L) r : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) (↑s : R) : L) ((algebraMap R L : (a : R) → L) r : L)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r

Tactic:
rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one,
    Submonoid.coe_one, ← (IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul]

Premises used: IsLocalization.mk'_eq_iff_eq, Submonoid.coe_one, map_mul, IsUnit.mul_left_cancel, HPow.hPow, IsLocalization.mk'_one, IsLocalization.map_units, mul_one
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
⊢ IsArtinianRing L

Tactic:
(localization_surjective S L).isArtinianRing

Premises used: IsArtinianRing.localization_surjective, Function.Surjective.isArtinianRing
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
⊢ IsArtinianRing.{u_1} (Localization (M := R) S)

Tactic:
localization_artinian S _

Premises used: IsArtinianRing.localization_artinian
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
mp : IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
mpr : (∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})) → IsBezout R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})

Tactic:
constructor
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (R := R) (Ideal.span {x, y})

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
mpr : ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I
⊢ IsBezout R

Tactic:
constructor
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
mpr : ∀ (x : R), Submodule.IsPrincipal (M := R) (R ∙ x)
mpr₁ : ∀ (N₁ N₂ : Submodule R R) (hN₁ : N₁.FG) (hN₂ : N₂.FG), N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal
⊢ ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I

Tactic:
apply Submodule.fg_induction

Premises used: Submodule.fg_induction
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ ∀ (x : R), Submodule.IsPrincipal (M := R) (R ∙ x)

Tactic:
fun _ => ⟨⟨_, rfl⟩⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ ∀ (x : R), Submodule.IsPrincipal (M := R) (R ∙ x)

Tactic:
exact fun _ => ⟨⟨_, rfl⟩⟩
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
x : R
hN₁ : Submodule.FG (M := R) (R ∙ x)
y : R
hN₂ : Submodule.FG (M := R) (R ∙ y)
mpr : Submodule.IsPrincipal (M := R) (Submodule.span R {x, y})
⊢ Submodule.IsPrincipal (M := R) (R ∙ x ⊔ R ∙ y)

Tactic:
rw [← Submodule.span_insert]

Premises used: Submodule.span_insert
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
x : R
hN₁ : Submodule.FG (M := R) (R ∙ x)
y : R
hN₂ : Submodule.FG (M := R) (R ∙ y)
⊢ Submodule.IsPrincipal (M := R) (Submodule.span R {x, y})

Tactic:
H _ _
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
x : R
hN₁ : Submodule.FG (M := R) (R ∙ x)
y : R
hN₂ : Submodule.FG (M := R) (R ∙ y)
⊢ Submodule.IsPrincipal (M := R) (Submodule.span R {x, y})

Tactic:
exact H _ _
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
mp : IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
mpr mpr₁ : (∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})) → IsBezout R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})

Tactic:
classical
    constructor
    · intro H x y; infer_instance
    · intro H
      constructor
      apply Submodule.fg_induction
      · exact fun _ => ⟨⟨_, rfl⟩⟩
      · rintro _ _ _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩
        rw [← Submodule.span_insert]
        exact H _ _

Premises used: Submodule.fg_induction, Submodule.span_insert, rfl
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsBezout R
rw : ∀ (x y : S), Submodule.IsPrincipal (R := S) (Ideal.span {x, y})
⊢ IsBezout S

Tactic:
rw [iff_span_pair_isPrincipal]

Premises used: IsBezout.iff_span_pair_isPrincipal
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsBezout R
x y : S
obtain :
  ∀ (x y : R),
    Submodule.IsPrincipal (R := S)
      (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
⊢ Submodule.IsPrincipal (R := S) (Ideal.span {x, y})

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y

Premises used: rfl
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsBezout R
x y : R
h :
  Eq (α := Submodule S S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))
⊢ Submodule.IsPrincipal (R := S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))

Tactic:
use f (gcd x y)

Premises used: IsBezout.gcd, DFunLike.coe
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsBezout R
x y : R
trans :
  Eq (α := Ideal S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Ideal.map (R := R) f (Ideal.span {gcd x y}))
trans₁ :
  Eq (α := Ideal S) (Ideal.map (R := R) f (Ideal.span {gcd x y}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))
⊢ Eq (α := Submodule S S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))

Tactic:
trans Ideal.map f (Ideal.span {gcd x y})

Premises used: IsBezout.gcd, Ideal.map, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsBezout R
x y : R
rw :
  Eq (α := Ideal S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Ideal.map (R := R) f (Ideal.span {x, y}))
rw₁ :
  Eq (α := Ideal S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Ideal.span (Set.image (α := R) (⇑f : (a : R) → S) {x, y}))
rw₂ :
  Eq (α := Ideal S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (Set.image (α := R) (⇑f : (a : R) → S) {y})))
rw₃ rw₄ :
  Eq (α := Ideal S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
⊢ Eq (α := Ideal S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
    (Ideal.map (R := R) f (Ideal.span {gcd x y}))

Tactic:
rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]

Premises used: Set.image_singleton, Ideal.map_span, Set.image_insert_eq, IsBezout.span_gcd
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
inst_2 : IsBezout R
x y : R
rw :
  Eq (α := Ideal S) (Ideal.span (Set.image (α := R) (⇑f : (a : R) → S) {gcd x y}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))
rw₁ rw₂ :
  Eq (α := Ideal S) (Ideal.span (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))
⊢ Eq (α := Ideal S) (Ideal.map (R := R) f (Ideal.span {gcd x y}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) (gcd x y) : S)))

Tactic:
rw [Ideal.map_span, Set.image_singleton]

Premises used: Set.image_singleton, Ideal.map_span
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
⊢ IsNoetherianRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
⊢ IsPrincipalIdealRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
⊢ ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
⊢ ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R

Tactic:
tfae_have 1 → 2
    | _ => inferInstance
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
⊢ UniqueFactorizationMonoid R

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
⊢ ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
⊢ ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R

Tactic:
tfae_have 2 → 3
    | _ => inferInstance
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
⊢ UniqueFactorizationMonoid R

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
⊢ WfDvdMonoid R

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
⊢ ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
⊢ ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R

Tactic:
tfae_have 3 → 4
    | _ => inferInstance
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
⊢ WfDvdMonoid R

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
⊢ IsNoetherianRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
⊢ ∀ (a : WfDvdMonoid R), IsNoetherianRing R

Tactic:
4 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
rw : WellFoundedGT.{u} { N : Submodule R R // N.FG }
⊢ IsNoetherianRing R

Tactic:
rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]

Premises used: isNoetherian_iff_fg_wellFounded, isNoetherianRing_iff
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
⊢ WellFoundedGT.{u} { N : Submodule R R // N.FG }

Tactic:
⟨RelEmbedding.wellFounded ?_ h⟩

Premises used: IsWellFounded.mk, RelEmbedding.wellFounded
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
refine : RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit
⊢ WellFoundedGT.{u} { N : Submodule R R // N.FG }

Tactic:
refine ⟨RelEmbedding.wellFounded ?_ h⟩
-- Module: Mathlib.RingTheory.Bezout
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
h : WellFounded.{u + 1} (α := R) DvdNotUnit
⊢ ∀ (I : { J : Ideal R // J.FG }), ∃ (x : R), (↑I : Ideal R) = Ideal.span {x}

Tactic:
have : ∀ I : { J : Ideal R // J.FG }, ∃ x : R, (I : Ideal R) = Ideal.span {x} :=
        fun ⟨I, hI⟩ => (IsBezout.isPrincipal_of_FG I hI).1