-- Mathlib/RingTheory/Bezout.lean
theorem iff_span_pair_isPrincipal :
    IsBezout R ↔ ∀ x y : R, (Ideal.span {x, y} : Ideal R).IsPrincipal

Proof state:
case mpr.isPrincipal_of_FG.h₁
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (x : R), (Submodule.span R {x}).IsPrincipal

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

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R

Tactic:
constructor

Result:
case mpr.isPrincipal_of_FG
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I

Proof state:
case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

Tactic:
intro H x y

Result:
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})

Proof state:
case mpr.isPrincipal_of_FG.h₂
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (M₁ M₂ : Submodule R R), M₁.IsPrincipal → M₂.IsPrincipal → (M₁ ⊔ M₂).IsPrincipal

Tactic:
rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩

Result:
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ (Submodule.span R {x} ⊔ Submodule.span R {y}).IsPrincipal

Proof state:
case mpr.isPrincipal_of_FG
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), I.FG → Submodule.IsPrincipal I

Tactic:
apply Submodule.fg_induction

Result:
case mpr.isPrincipal_of_FG.h₁
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (x : R), (Submodule.span R {x}).IsPrincipal

case mpr.isPrincipal_of_FG.h₂
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (M₁ M₂ : Submodule R R), M₁.IsPrincipal → M₂.IsPrincipal → (M₁ ⊔ M₂).IsPrincipal

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R

Tactic:
intro H

Result:
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R

Proof state:
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ (Submodule.span R {x, y}).IsPrincipal

Tactic:
exact H _ _

Result:
no goals

Proof state:
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ (Submodule.span R {x} ⊔ Submodule.span R {y}).IsPrincipal

Tactic:
rw [← Submodule.span_insert]

Result:
case mpr.isPrincipal_of_FG.h₂.mk.intro.mk.intro
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
x y : R
⊢ (Submodule.span R {x, y}).IsPrincipal