Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f f' : M [⋀^ι]→ₗ[R] N
g✝ g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
g : M [⋀^ι]→ₗ[R] N
toFun✝ : (ι → M) → N
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
map_eq_zero_of_eq'✝ :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }.toFun v = 0
h :
  (fun f ↦ f.toFun)
      { 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 ↦ f.toFun) 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'✝ } =
    g

Tactic:
rcases g with ⟨⟨_, _, _⟩, _⟩

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
toFun✝¹ : (ι → M) → N
map_update_add'✝¹ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
    toFun✝¹ (update m i (x + y)) = toFun✝¹ (update m i x) + toFun✝¹ (update m i y)
map_update_smul'✝¹ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M),
    toFun✝¹ (update m i (c • x)) = c • toFun✝¹ (update m i x)
map_eq_zero_of_eq'✝¹ :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        { toFun := toFun✝¹, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹ }.toFun v = 0
toFun✝ : (ι → M) → N
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
map_eq_zero_of_eq'✝ :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }.toFun v = 0
h :
  (fun f ↦ f.toFun)
      { 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 ↦ f.toFun)
      { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝,
        map_eq_zero_of_eq' := map_eq_zero_of_eq'✝ }
⊢ { toFun := toFun✝¹, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹,
      map_eq_zero_of_eq' := map_eq_zero_of_eq'✝¹ } =
    { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝,
      map_eq_zero_of_eq' := map_eq_zero_of_eq'✝ }