-- Mathlib/LinearAlgebra/Multilinear/Curry.lean
theorem curryFinFinset_symm_apply_piecewise_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k)
    (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂))
    (x y : M') :
    (curryFinFinset R M₂ M' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) =
      f (fun _ => x) fun _ => y

Proof state:
case h.e_5.h.h.e_6.h.h.hi
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin k
⊢ (s.orderEmbOfFin hk) x✝ ∈ s

Tactic:
apply Finset.orderEmbOfFin_mem

Result:
no goals

Proof state:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) = (f fun x_1 => x) fun x => y

Tactic:
rw [curryFinFinset_symm_apply]

Result:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ ((f fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i =>
      s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) =
    (f fun x_1 => x) fun x => y

Proof state:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ ((f fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i =>
      s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) =
    (f fun x_1 => x) fun x => y

Tactic:
congr

Result:
case h.e_5.h.h.e_6.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ (fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) = fun x_1 => x

case h.e_6.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ (fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x => y

Proof state:
case h.e_6.h.h.hi
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin l
⊢ (sᶜ.orderEmbOfFin hl) x✝ ∉ s

Tactic:
exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

Result:
no goals

Proof state:
case h.e_5.h.h.e_6.h.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin k
⊢ s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl x✝)) = x

Tactic:
rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]

Result:
case h.e_5.h.h.e_6.h.h.hi
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin k
⊢ (s.orderEmbOfFin hk) x✝ ∈ s

Proof state:
case h.e_5.h.h.e_6.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ (fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) = fun x_1 => x

Tactic:
ext

Result:
case h.e_5.h.h.e_6.h.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin k
⊢ s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl x✝)) = x

Proof state:
case h.e_6.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ (fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x => y

Tactic:
ext

Result:
case h.e_6.h.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin l
⊢ s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr x✝)) = y

Proof state:
case h.e_6.h.h
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin l
⊢ s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr x✝)) = y

Tactic:
rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_not_mem]

Result:
case h.e_6.h.h.hi
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
x✝ : Fin l
⊢ (sᶜ.orderEmbOfFin hl) x✝ ∉ s