-- Mathlib/LinearAlgebra/Prod.lean
theorem range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f ⊔ ker g = ⊤) :
    range (prod f g) = (range f).prod (range g)

Proof state:
case intro.intro.intro.intro.refine_2
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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
⊢ g (x' + x) = g y

Tactic:
simp [← eq_sub_iff_add_eq.1 H, map_add, add_left_inj, self_eq_add_right, mem_ker.mp hy']

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 (f.prod g) = (range f).prod (range g)

Tactic:
refine le_antisymm (f.range_prod_le g) ?_

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 f).prod (range g) ≤ range (f.prod g)

Proof state:
case intro.intro.intro.intro.refine_1
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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

Tactic:
rwa [add_sub_cancel_right]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 ∧ g y_1 = g y

Tactic:
have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 ∧ g y_1 = g y

Proof state:
case intro.intro.intro.intro
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 ∧ g y_1 = g y

Tactic:
refine ⟨x' + x, ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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
M : Type v
M₂ : Type w
M₃ : Type y
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
⊢ g (x' + x) = g y

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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

Tactic:
simp only [h, mem_top]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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)

Tactic:
rintro _ _ x rfl y rfl

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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)

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 ∧ g y_1 = g y

Tactic:
rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩

Result:
case intro.intro.intro.intro
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 ∧ g y_1 = g y

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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)

Tactic:
simp only [Prod.mk.inj_iff, ← sub_mem_ker_iff (f := f)]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 ∧ g y_1 = g y

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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 f).prod (range g) ≤ range (f.prod g)

Tactic:
simp only [SetLike.le_def, prod_apply, mem_range, SetLike.mem_coe, mem_prod, exists_imp, and_imp,
  Prod.forall, Pi.prod]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
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)