awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
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)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have h : IsLocalization.mk' L 1 s = IsLocalization.mk' (M := S) L r 1
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]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
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
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
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)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
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)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have h₃ : Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) 1 : L) ((algebraMap R L : (a : R) → L) ((↑s : R) * r) : L)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
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)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
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)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
have mp : IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
mp : IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
have mpr : (∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})) → IsBezout R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ IsBezout R
have mpr : ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I
have mpr : ∀ (x : R), Submodule.IsPrincipal (M := R) (R ∙ x)
Tactic: apply Submodule.fg_induction
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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)
⊢ ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I
have mpr₁ : ∀ (N₁ N₂ : Submodule R R) (hN₁ : N₁.FG) (hN₂ : N₂.FG), N₁.IsPrincipal → N₂.IsPrincipal → (N₁ ⊔ N₂).IsPrincipal
Tactic: apply Submodule.fg_induction
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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) (R ∙ x ⊔ R ∙ y)
have mpr : Submodule.IsPrincipal (M := R) (Submodule.span R {x, y})
Tactic: rw [← Submodule.span_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
have mp : 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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
Goal:
R : Type u
inst : CommRing R
mp : IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})
have mpr : (∀ (x y : R), Submodule.IsPrincipal (R := R) (Ideal.span {x, y})) → IsBezout R
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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ IsBezout S
have rw : ∀ (x y : S), Submodule.IsPrincipal (R := S) (Ideal.span {x, y})
Tactic: rw [iff_span_pair_isPrincipal]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ Submodule.IsPrincipal (R := S) (Ideal.span {x, y})
have 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))))
Tactic: obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ Submodule.IsPrincipal (R := S)
    (Ideal.span (insert (α := S) ((f : (a : R) → S) x : S) (singleton (α := S) ((f : (a : R) → S) y : S))))
have 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)))
Tactic: use f (gcd x y)
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ 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)))
have 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}))
Tactic: trans Ideal.map f (Ideal.span {gcd x y})
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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}))
⊢ 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)))
have 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)))
Tactic: trans Ideal.map f (Ideal.span {gcd x y})
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ 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}))
have 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}))
Tactic: rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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}))
⊢ 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}))
have 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}))
Tactic: rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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}))
⊢ 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}))
have 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})))
Tactic: rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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})))
⊢ 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}))
have 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))))
Tactic: rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [Ideal.map_span, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [Ideal.map_span, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
Tactic: tfae_have 1 → 2
    | _ => inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
tfae_1_to_2 : ∀ (a : IsNoetherianRing R), IsPrincipalIdealRing R
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have tfae_2_to_3 : ∀ (a : IsPrincipalIdealRing R), UniqueFactorizationMonoid R
Tactic: tfae_have 2 → 3
    | _ => inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (hypothesis)
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
⊢ [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
have tfae_3_to_4 : ∀ (a : UniqueFactorizationMonoid R), WfDvdMonoid R
Tactic: tfae_have 3 → 4
    | _ => inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
⊢ IsNoetherianRing R
have rw : WellFoundedGT.{u} { N : Submodule R R // N.FG }
Tactic: rw [isNoetherianRing_iff, isNoetherian_iff_fg_wellFounded]
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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 }
have refine : RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit
Tactic: refine ⟨RelEmbedding.wellFounded ?_ h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (hypothesis)
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
⊢ RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
this : ∀ (I : { J : Ideal R // J.FG }), ∃ (x : R), (↑I : Ideal R) = Ideal.span {x}
⊢ RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit
have choose : (f : (I : { J : Ideal R // J.FG }) → R) →
  (hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}) →
    RelEmbedding (β := R) (fun (x1 x2 : { N : Submodule R R // N.FG }) ↦ x2 < x1) DvdNotUnit
Tactic: choose f hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Bezout (goal)
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
f : (I : { J : Ideal R // J.FG }) → R
hf : ∀ (I : { J : Ideal R // J.FG }), (↑I : Ideal R) = Ideal.span {f I}
x y : { N : Submodule R R // N.FG }
e : f x = f y
⊢ x = y
have a : (↑x : Submodule R R) = (↑y : Submodule R R)
Tactic: ext1