R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
⊢ Submodule.prod (range f) (range g) ≤ range (prod f g)
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
⊢ range (prod f g) = Submodule.prod (range f) (range g)
refine' le_antisymm (f.range_prod_le g) _
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
⊢ ∀ (a : M₂) (b : M₃) (x : M), ↑f x = a → ∀ (x : M), ↑g x = b → ∃ y, (↑f y, ↑g y) = (a, b)
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
⊢ Submodule.prod (range f) (range g) ≤ range (prod f g)
simp only [SetLike.le_def, prod_apply, mem_range, SetLike.mem_coe, mem_prod, exists_imp, and_imp,
  Prod.forall, Pi.prod]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
⊢ ∃ y_1, (↑f y_1, ↑g y_1) = (↑f x, ↑g y)
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
⊢ ∀ (a : M₂) (b : M₃) (x : M), ↑f x = a → ∀ (x : M), ↑g x = b → ∃ y, (↑f y, ↑g y) = (a, b)
rintro _ _ x rfl y rfl
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
⊢ ∃ y_1, y_1 - x ∈ ker f ∧ y_1 - y ∈ ker g
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
⊢ ∃ y_1, (↑f y_1, ↑g y_1) = (↑f x, ↑g y)
simp only [Prod.mk.inj_iff, ← sub_mem_ker_iff]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
⊢ ∃ y_1, y_1 - x ∈ ker f ∧ y_1 - y ∈ ker g
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
⊢ ∃ y_1, y_1 - x ∈ ker f ∧ y_1 - y ∈ ker g
have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
case intro.intro.intro.intro
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
x' : M
hx' : x' ∈ ker f
y' : M
hy' : y' ∈ ker g
H : x' + y' = y - x
⊢ ∃ y_1, y_1 - x ∈ ker f ∧ y_1 - y ∈ ker g
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
⊢ ∃ y_1, y_1 - x ∈ ker f ∧ y_1 - y ∈ ker g
rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩
case intro.intro.intro.intro.refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
x' : M
hx' : x' ∈ ker f
y' : M
hy' : y' ∈ ker g
H : x' + y' = y - x
⊢ x' + x - x ∈ ker f

case intro.intro.intro.intro.refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
x' : M
hx' : x' ∈ ker f
y' : M
hy' : y' ∈ ker g
H : x' + y' = y - x
⊢ x' + x - y ∈ ker g
case intro.intro.intro.intro
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
x' : M
hx' : x' ∈ ker f
y' : M
hy' : y' ∈ ker g
H : x' + y' = y - x
⊢ ∃ y_1, y_1 - x ∈ ker f ∧ y_1 - y ∈ ker g
refine' ⟨x' + x, _, _⟩
no goals
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
⊢ y - x ∈ ker f ⊔ ker g
simp only [h, mem_top]
no goals
case intro.intro.intro.intro.refine'_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
x' : M
hx' : x' ∈ ker f
y' : M
hy' : y' ∈ ker g
H : x' + y' = y - x
⊢ x' + x - x ∈ ker f
rwa [add_sub_cancel]
no goals
case intro.intro.intro.intro.refine'_2
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.481077
M₆ : Type ?u.481080
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : ker f ⊔ ker g = ⊤
x y : M
this : y - x ∈ ker f ⊔ ker g
x' : M
hx' : x' ∈ ker f
y' : M
hy' : y' ∈ ker g
H : x' + y' = y - x
⊢ x' + x - y ∈ ker g
simp [← eq_sub_iff_add_eq.1 H, map_add, add_left_inj, self_eq_add_right, mem_ker.mp hy']