-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma domDomRestrict_aux {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
    [DecidableEq {a // P a}]
    (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) (i : {a : ι // P a})
    (c : M₁ i) : (fun j ↦ if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c

Proof state:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : j = ↑i
⊢ (if h : P ↑i then update x i c ⟨↑i, h⟩ else z ⟨↑i, h⟩) = c

Tactic:
simp only [i.2, update_self, dite_true]

Result:
no goals

Proof state:
case neg
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : ¬P j
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) = if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩

Tactic:
simp only [h', ne_eq, Subtype.mk.injEq, dite_false]

Result:
no goals

Proof state:
case neg
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) = if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩

Tactic:
by_cases h' : P j

Result:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) = if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩

case neg
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : ¬P j
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) = if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩

Proof state:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
⊢ update x i c ⟨j, ⋯⟩ = x ⟨j, ⋯⟩

Tactic:
have h'' : ¬ ⟨j, h'⟩ = i :=
  fun he => by apply_fun (fun x => x.1) at he; exact h he

Result:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
h'' : ¬⟨j, h'⟩ = i
⊢ update x i c ⟨j, ⋯⟩ = x ⟨j, ⋯⟩

Proof state:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
h'' : ¬⟨j, h'⟩ = i
⊢ update x i c ⟨j, ⋯⟩ = x ⟨j, ⋯⟩

Tactic:
rw [Function.update_of_ne h'']

Result:
no goals

Proof state:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) = if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩

Tactic:
simp only [h', ne_eq, Subtype.mk.injEq, dite_true]

Result:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
⊢ update x i c ⟨j, ⋯⟩ = x ⟨j, ⋯⟩

Proof state:
case neg
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c j

Tactic:
rw [Function.update_of_ne h]

Result:
case neg
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) = if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩

Proof state:
case h
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c j

Tactic:
by_cases h : j = i

Result:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : j = ↑i
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c j

case neg
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c j

Proof state:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : j = ↑i
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c j

Tactic:
rw [h, Function.update_self]

Result:
case pos
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : j = ↑i
⊢ (if h : P ↑i then update x i c ⟨↑i, h⟩ else z ⟨↑i, h⟩) = c

Proof state:
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
⊢ (fun j => if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c

Tactic:
ext j

Result:
case h
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
⊢ (if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c j

Proof state:
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
he : ↑⟨j, h'⟩ = ↑i
⊢ False

Tactic:
exact h he

Result:
no goals