Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case mk.mk
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
toFun✝¹ : ((i : ι) → M₁ i) → M₂
map_update_add'✝¹ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝¹ (update m i (x + y)) = toFun✝¹ (update m i x) + toFun✝¹ (update m i y)
map_update_smul'✝¹ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝¹ (update m i (c • x)) = c • toFun✝¹ (update m i x)
toFun✝ : ((i : ι) → M₁ i) → M₂
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }
⊢ { toFun := toFun✝¹, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹ } =
    { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁰ : Semiring R
inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
f f' : MultilinearMap R M₁ M₂
toFun✝¹ : ((i : ι) → M₁ i) → M₂
map_update_add'✝¹ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝¹ (update m i (x + y)) = toFun✝¹ (update m i x) + toFun✝¹ (update m i y)
map_update_smul'✝¹ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝¹ (update m i (c • x)) = c • toFun✝¹ (update m i x)
toFun✝ : ((i : ι) → M₁ i) → M₂
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }
⊢ { toFun := toFun✝¹, map_update_add' := map_update_add'✝¹, map_update_smul' := map_update_smul'✝¹ } =
    { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }