-- Mathlib/LinearAlgebra/Pi.lean
theorem le_comap_single_pi [DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {i} :
    p i ≤ Submodule.comap (LinearMap.single R φ i : φ i →ₗ[R] _) (Submodule.pi Set.univ p)

Proof state:
case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : ¬j = i
⊢ (single R φ i) x j ∈ p j

Tactic:
rw [LinearMap.coe_single, Pi.single_eq_of_ne h]

Result:
case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : ¬j = i
⊢ 0 ∈ p j

Proof state:
case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : j = i
⊢ (single R φ i) x j ∈ p j

Tactic:
rwa [h, LinearMap.coe_single, Pi.single_eq_same]

Result:
no goals

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
⊢ p i ≤ comap (single R φ i) (pi Set.univ p)

Tactic:
intro x hx

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
⊢ x ∈ comap (single R φ i) (pi Set.univ p)

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
⊢ x ∈ comap (single R φ i) (pi Set.univ p)

Tactic:
rw [Submodule.mem_comap, Submodule.mem_pi]

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
⊢ ∀ i_1 ∈ Set.univ, (single R φ i) x i_1 ∈ p i_1

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ (single R φ i) x j ∈ p j

Tactic:
by_cases h : j = i

Result:
case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : j = i
⊢ (single R φ i) x j ∈ p j

case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : ¬j = i
⊢ (single R φ i) x j ∈ p j

Proof state:
case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
h : ¬j = i
⊢ 0 ∈ p j

Tactic:
exact (p j).zero_mem

Result:
no goals

Proof state:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
⊢ ∀ i_1 ∈ Set.univ, (single R φ i) x i_1 ∈ p i_1

Tactic:
rintro j -

Result:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ (single R φ i) x j ∈ p j