-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem LinearIndependent.inl_union_inr {s : Set M} {t : Set M'}
    (hs : LinearIndependent R (fun x => x : s → M))
    (ht : LinearIndependent R (fun x => x : t → M')) :
    LinearIndependent R (fun x => x : ↥(inl R M M' '' s ∪ inr R M M' '' t) → M × M')

Proof state:
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
⊢ Injective (Sum.elim (fun i => ⟨(inl R M M') ↑i, ⋯⟩) fun i => ⟨(inr R M M') ↑i, ⋯⟩)

Tactic:
rintro (_|_) (_|_) eq <;> simp [hs.ne_zero, ht.ne_zero] at eq <;> aesop

Result:
no goals

Proof state:
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) :=
  Equiv.ofBijective (Sum.elim (fun i => ⟨(inl R M M') ↑i, ⋯⟩) fun i => ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ (fun x => ↑x) ∘ ⇑e = Sum.elim (⇑(inl R M M') ∘ fun x => ↑x) (⇑(inr R M M') ∘ fun x => ↑x)

Tactic:
ext (_ | _) <;> rfl

Result:
no goals

Proof state:
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
⊢ Surjective (Sum.elim (fun i => ⟨(inl R M M') ↑i, ⋯⟩) fun i => ⟨(inr R M M') ↑i, ⋯⟩)

Tactic:
rintro ⟨_, ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩⟩ <;> aesop

Result:
no goals

Proof state:
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
⊢ LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) => ↑x

Tactic:
let e : s ⊕ t ≃ ↥(inl R M M' '' s ∪ inr R M M' '' t) :=
  .ofBijective (Sum.elim (fun i ↦ ⟨_, .inl ⟨_, i.2, rfl⟩⟩) fun i ↦ ⟨_, .inr ⟨_, i.2, rfl⟩⟩)
    ⟨by rintro (_|_) (_|_) eq <;> simp [hs.ne_zero, ht.ne_zero] at eq <;> aesop,
      by rintro ⟨_, ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩⟩ <;> aesop⟩

Result:
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) :=
  Equiv.ofBijective (Sum.elim (fun i => ⟨(inl R M M') ↑i, ⋯⟩) fun i => ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) => ↑x

Proof state:
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) :=
  Equiv.ofBijective (Sum.elim (fun i => ⟨(inl R M M') ↑i, ⋯⟩) fun i => ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) => ↑x

Tactic:
refine (linearIndependent_equiv' e ?_).mp (linearIndependent_inl_union_inr' hs ht)

Result:
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) :=
  Equiv.ofBijective (Sum.elim (fun i => ⟨(inl R M M') ↑i, ⋯⟩) fun i => ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ (fun x => ↑x) ∘ ⇑e = Sum.elim (⇑(inl R M M') ∘ fun x => ↑x) (⇑(inr R M M') ∘ fun x => ↑x)

Proof state:
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
⊢ LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) => ↑x

Tactic:
nontriviality R

Result:
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
⊢ LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) => ↑x