Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).1

pp: case inl.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).2

pp: case inr.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).1

pp: case inr.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).2

Tactic:
<;>

Goal state after:
case inl.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).1

case inl.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).2

case inr.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).1

case inr.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).2