-- Mathlib/LinearAlgebra/Multilinear/Pi.lean
theorem piFamily_single_left_apply [Fintype ι] [∀ i, DecidableEq (κ i)]
    (p : Π i, κ i) (f : MultilinearMap R (fun i ↦ M i (p i)) (N p)) (x : Π i j, M i j) :
    piFamily (Pi.single p f) x = Pi.single p (f fun i => x i (p i))

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
⊢ (piFamily (Pi.single p f)) x = Pi.single p (f fun i => x i (p i))

Tactic:
ext p'

Result:
case h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
⊢ (piFamily (Pi.single p f)) x p' = Pi.single p (f fun i => x i (p i)) p'

Proof state:
case h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
⊢ (piFamily (Pi.single p f)) x p' = Pi.single p (f fun i => x i (p i)) p'

Tactic:
obtain rfl | hp := eq_or_ne p p'

Result:
case h.inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
⊢ (piFamily (Pi.single p f)) x p = Pi.single p (f fun i => x i (p i)) p

case h.inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ (piFamily (Pi.single p f)) x p' = Pi.single p (f fun i => x i (p i)) p'

Proof state:
case h.inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ (piFamily (Pi.single p f)) x p' = Pi.single p (f fun i => x i (p i)) p'

Tactic:
simp [hp]

Result:
no goals

Proof state:
case h.inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i => M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
⊢ (piFamily (Pi.single p f)) x p = Pi.single p (f fun i => x i (p i)) p

Tactic:
simp

Result:
no goals