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
R : Type u
inst✝ : CommRing R
⊢ IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
constructor
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
case mp
R : Type u
inst✝ : CommRing R
⊢ IsBezout R → ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
intro H x y
no goals
case mp
R : Type u
inst✝ : CommRing R
H : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
infer_instance
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R
case mpr
R : Type u
inst✝ : CommRing R
⊢ (∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})) → IsBezout R
intro H
case mpr.isPrincipal_of_FG
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), Ideal.FG I → Submodule.IsPrincipal I
case mpr
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ IsBezout R
constructor
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.IsPrincipal (Submodule.span R {x})

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), Submodule.IsPrincipal M₁ → Submodule.IsPrincipal M₂ → Submodule.IsPrincipal (M₁ ⊔ M₂)
case mpr.isPrincipal_of_FG
R : Type u
inst✝ : CommRing R
H : ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
⊢ ∀ (I : Ideal R), Ideal.FG I → Submodule.IsPrincipal I
apply Submodule.fg_induction
no goals
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.IsPrincipal (Submodule.span R {x})
exact fun _ => ⟨⟨_, rfl⟩⟩
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.IsPrincipal (Submodule.span R {x} ⊔ Submodule.span R {y})
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), Submodule.IsPrincipal M₁ → Submodule.IsPrincipal M₂ → Submodule.IsPrincipal (M₁ ⊔ M₂)
rintro _ _ ⟨⟨x, rfl⟩⟩ ⟨⟨y, rfl⟩⟩
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.IsPrincipal (Submodule.span R {x, y})
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.IsPrincipal (Submodule.span R {x} ⊔ Submodule.span R {y})
rw [← Submodule.span_insert]
no goals
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.IsPrincipal (Submodule.span R {x, y})
exact H _ _