-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f f' : M [⋀^ι]→ₗ[R] N
g_1 g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
g : M [⋀^ι]→ₗ[R] N
toFun : ((i : ι) → M) → N
map_update_add' :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M) (i : ι) (x y : M),
    toFun (update (β := fun (x : ι) ↦ M) m i (x + y)) =
      toFun (update (β := fun (x : ι) ↦ M) m i x) + toFun (update (β := fun (x : ι) ↦ M) m i y)
map_update_smul' :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M) (i : ι) (c : R) (x : M),
    toFun (update (β := fun (x : ι) ↦ M) m i (c • x)) = c • toFun (update (β := fun (x : ι) ↦ M) m i x)
map_eq_zero_of_eq' :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        (MultilinearMap.mk (M₁ := fun (x : ι) ↦ M) toFun map_update_add' map_update_smul').toFun (M₁ := fun (x : ι) ↦ M)
            v =
          0
h :
  Eq (α := (a : ι → M) → N)
    ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M))
      { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul',
        map_eq_zero_of_eq' := map_eq_zero_of_eq' })
    ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M)) g)
⊢ { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul',
      map_eq_zero_of_eq' := map_eq_zero_of_eq' : M [⋀^ι]→ₗ[R] N } =
    g
have rcases : ∀ (toFun_1 : ((i : ι) → M) → N)
  (map_update_add'_1 :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M) (i : ι) (x y : M),
      toFun_1 (update (β := fun (x : ι) ↦ M) m i (x + y)) =
        toFun_1 (update (β := fun (x : ι) ↦ M) m i x) + toFun_1 (update (β := fun (x : ι) ↦ M) m i y))
  (map_update_smul'_1 :
    ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M) (i : ι) (c : R) (x : M),
      toFun_1 (update (β := fun (x : ι) ↦ M) m i (c • x)) = c • toFun_1 (update (β := fun (x : ι) ↦ M) m i x))
  (map_eq_zero_of_eq'_1 :
    ∀ (v : ι → M) (i j : ι),
      v i = v j →
        i ≠ j →
          (MultilinearMap.mk (M₁ := fun (x : ι) ↦ M) toFun_1 map_update_add'_1 map_update_smul'_1).toFun (M₁ :=
              fun (x : ι) ↦ M) v =
            0)
  (h :
    Eq (α := (a : ι → M) → N)
      ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M))
        { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul',
          map_eq_zero_of_eq' := map_eq_zero_of_eq' })
      ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M))
        { toFun := toFun_1, map_update_add' := map_update_add'_1, map_update_smul' := map_update_smul'_1,
          map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 })),
  { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul',
      map_eq_zero_of_eq' := map_eq_zero_of_eq' : M [⋀^ι]→ₗ[R] N } =
    { toFun := toFun_1, map_update_add' := map_update_add'_1, map_update_smul' := map_update_smul'_1,
      map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 }
Tactic: rcases g with ⟨⟨_, _, _⟩, _⟩
Cleared hypotheses: g, h