-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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_1 : 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')) ⋯)
    ⋯
h :
  ∀ (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
⊢ 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')))
have h₁ : ∀ (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: ext (_ | _)