R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ ∀ (x y : S), Submodule.IsPrincipal (Ideal.span {x, y})
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ IsBezout S
rw [iff_span_pair_isPrincipal]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : S
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
⊢ ∀ (x y : S), Submodule.IsPrincipal (Ideal.span {x, y})
intro x y
case intro.intro
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {↑f x, ↑f y})
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : S
⊢ Submodule.IsPrincipal (Ideal.span {x, y})
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hf x, hf y
case intro.intro
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Submodule.span S {↑f (gcd x y)}
case intro.intro
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Submodule.IsPrincipal (Ideal.span {↑f x, ↑f y})
use f (gcd x y)
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Ideal.map f (Ideal.span {gcd x y})

R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = Submodule.span S {↑f (gcd x y)}
case intro.intro
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Submodule.span S {↑f (gcd x y)}
trans Ideal.map f (Ideal.span {gcd x y})
no goals
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f x, ↑f y} = Ideal.map f (Ideal.span {gcd x y})
rw [span_gcd, Ideal.map_span, Set.image_insert_eq, Set.image_singleton]
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f (gcd x y)} = Submodule.span S {↑f (gcd x y)}
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.map f (Ideal.span {gcd x y}) = Submodule.span S {↑f (gcd x y)}
rw [Ideal.map_span, Set.image_singleton]
no goals
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
inst✝ : IsBezout R
x y : R
⊢ Ideal.span {↑f (gcd x y)} = Submodule.span S {↑f (gcd x y)}
rfl