awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val val_1 : (↑s : Type u_4)
eq :
  Eq (α := (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inl val))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inl val_1))
⊢ (↑val : M) = (↑val_1 : M)

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

Premises used: LinearIndependent.ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val : (↑s : Type u_4)
val_1 : (↑t : Type u_5)
eq :
  Eq (α := (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inl val))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inr val_1))
⊢ Sum.inl val = Sum.inr val_1

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

Premises used: LinearIndependent.ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val : (↑t : Type u_5)
val_1 : (↑s : Type u_4)
eq :
  Eq (α := (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inr val))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inl val_1))
⊢ Sum.inr val = Sum.inl val_1

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

Premises used: LinearIndependent.ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val val_1 : (↑t : Type u_5)
eq :
  Eq (α := (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inr val))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inr val_1))
⊢ (↑val : M') = (↑val_1 : M')

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

Premises used: LinearIndependent.ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val val_1 : (↑s : Type u_4)
eq : (↑val : M) = (↑val_1 : M)
⊢ Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5)) (Sum.inl val) (Sum.inl val_1)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val val_1 : (↑t : Type u_5)
eq : (↑val : M') = (↑val_1 : M')
⊢ Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5)) (Sum.inr val) (Sum.inr val_1)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
w : M
left : w ∈ s
⊢ ∃ (a : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5)),
    Eq (α :=
      (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
      (Sum.elim
          (fun (i : (↑s : Type u_4)) ↦
            Subtype.mk (p := fun (x : M × M') ↦
              Membership.mem (γ := Set (M × M'))
                ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
              ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
          (fun (i : (↑t : Type u_5)) ↦
            Subtype.mk (p := fun (x : M × M') ↦
              Membership.mem (γ := Set (M × M'))
                ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
              ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
          a :
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
      (Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') w) ⋯ :
        { x : M × M' //
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x })

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
w : M'
left : w ∈ t
⊢ ∃ (a : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5)),
    Eq (α :=
      (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
      (Sum.elim
          (fun (i : (↑s : Type u_4)) ↦
            Subtype.mk (p := fun (x : M × M') ↦
              Membership.mem (γ := Set (M × M'))
                ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
              ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
          (fun (i : (↑t : Type u_5)) ↦
            Subtype.mk (p := fun (x : M × M') ↦
              Membership.mem (γ := Set (M × M'))
                ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
              ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
          a :
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
      (Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') w) ⋯ :
        { x : M × M' //
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x })

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
⊢ LinearIndependent R (M := M × M')
    fun
      (x :
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))) ↦
    (↑x : M × M')

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

Premises used: linearIndependent_equiv', linearIndependent_inl_union_inr', Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
refine :
  Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) → M × M')
    ((fun
          (x :
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5))) ↦
        (↑x : M × M')) ∘
      (⇑e :
        (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
          (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))))
    (Sum.elim (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
      (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')))
⊢ LinearIndependent R (M := M × M')
    fun
      (x :
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))) ↦
    (↑x : M × M')

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

Premises used: linearIndependent_equiv', linearIndependent_inl_union_inr', Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
val : (↑s : Type u_4)
⊢ Eq.{u_4 + 1} (α := M)
    (Function.comp (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5))
        (fun
            (x :
              (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
                Type (max u_4 u_5))) ↦
          (↑x : M × M'))
        (⇑e :
          (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5)))
        (Sum.inl val)).1
    (Sum.elim (β := (↑t : Type u_5))
        (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
        (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M'))
        (Sum.inl val)).1

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
val : (↑s : Type u_4)
⊢ Eq.{u_5 + 1} (α := M')
    (Function.comp (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5))
        (fun
            (x :
              (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
                Type (max u_4 u_5))) ↦
          (↑x : M × M'))
        (⇑e :
          (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5)))
        (Sum.inl val)).2
    (Sum.elim (β := (↑t : Type u_5))
        (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
        (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M'))
        (Sum.inl val)).2

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
val : (↑t : Type u_5)
⊢ Eq.{u_4 + 1} (α := M)
    (Function.comp (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5))
        (fun
            (x :
              (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
                Type (max u_4 u_5))) ↦
          (↑x : M × M'))
        (⇑e :
          (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5)))
        (Sum.inr val)).1
    (Sum.elim (α := (↑s : Type u_4))
        (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
        (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M'))
        (Sum.inr val)).1

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
val : (↑t : Type u_5)
⊢ Eq.{u_5 + 1} (α := M')
    (Function.comp (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5))
        (fun
            (x :
              (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
                Type (max u_4 u_5))) ↦
          (↑x : M × M'))
        (⇑e :
          (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5)))
        (Sum.inr val)).2
    (Sum.elim (α := (↑s : Type u_4))
        (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
        (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M'))
        (Sum.inr val)).2

Tactic:
rfl