R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {gcd x y}
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {x, y}
rw [← span_gcd]
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ {gcd x y}
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ Ideal.span {gcd x y}
apply Ideal.subset_span
no goals
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y : R
⊢ gcd x y ∈ {gcd x y}
simp