-- Mathlib/LinearAlgebra/Prod.lean
theorem le_prod_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} {q : Submodule R (M × M₂)} :
    q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Proof state:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ q ≤ p₁.prod p₂ → map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
intro h

Result:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Proof state:
case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩

Result:
case mp.right.intro.mk.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ ↑q
⊢ (LinearMap.snd R M M₂) (y1, y2) ∈ p₂

Proof state:
case mp.left.intro.mk.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ ↑q
⊢ (LinearMap.fst R M M₂) (y1, y2) ∈ p₁

Tactic:
exact (h hy1).1

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ q ≤ p₁.prod p₂ ↔ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
constructor

Result:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ q ≤ p₁.prod p₂ → map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂

Proof state:
case mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
constructor

Result:
case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁

case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂

Proof state:
case mpr.intro.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (LinearMap.fst R M M₂) q ≤ p₁
hK : map (LinearMap.snd R M M₂) q ≤ p₂
x1 : M
x2 : M₂
h : (x1, x2) ∈ q
⊢ (x1, x2) ∈ p₁.prod p₂

Tactic:
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Result:
no goals

Proof state:
case mp.right.intro.mk.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ ↑q
⊢ (LinearMap.snd R M M₂) (y1, y2) ∈ p₂

Tactic:
exact (h hy1).2

Result:
no goals

Proof state:
case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁

Tactic:
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩

Result:
case mp.left.intro.mk.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ ↑q
⊢ (LinearMap.fst R M M₂) (y1, y2) ∈ p₁

Proof state:
case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂

Tactic:
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h

Result:
case mpr.intro.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (LinearMap.fst R M M₂) q ≤ p₁
hK : map (LinearMap.snd R M M₂) q ≤ p₂
x1 : M
x2 : M₂
h : (x1, x2) ∈ q
⊢ (x1, x2) ∈ p₁.prod p₂