-- Mathlib/Data/Finset/Update.lean
theorem updateFinset_updateFinset {s t : Finset ι} (hst : Disjoint s t)
    {y : ∀ i : ↥s, π i} {z : ∀ i : ↥t, π i} :
    updateFinset (updateFinset x s y) t z =
    updateFinset x (s ∪ t) (Equiv.piFinsetUnion π hst ⟨y, z⟩)

Proof state:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False

Tactic:
exact Finset.disjoint_left.mp hst his hit

Result:
no goals

Proof state:
case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ y ⟨i, ⋯⟩ = if h : True ∨ False then (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩ else x i

Tactic:
exact piCongrLeft_sumInl (fun b : ↥(s ∪ t) => π b) e y z ⟨i, his⟩ |>.symm

Result:
no goals

Proof state:
case h
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
by_cases his : i ∈ s <;> by_cases hit : i ∈ t <;>
  simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

Result:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ z ⟨i, ⋯⟩ = if h : True ∨ True then (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩ else x i

case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ y ⟨i, ⋯⟩ = if h : True ∨ False then (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩ else x i

case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ z ⟨i, ⋯⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩

Proof state:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
⊢ updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z))

Tactic:
congr with i

Result:
case h
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Proof state:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ z ⟨i, ⋯⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩

Tactic:
exact piCongrLeft_sumInr (fun b : ↥(s ∪ t) => π b) e y z ⟨i, hit⟩ |>.symm

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
⊢ updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z))

Tactic:
set e := Equiv.Finset.union s t hst

Result:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
⊢ updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z))

Proof state:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ z ⟨i, ⋯⟩ = if h : True ∨ True then (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩ else x i

Tactic:
exfalso

Result:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
hst : Disjoint s t
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
e : { x // x ∈ s } ⊕ { x // x ∈ t } ≃ { x // x ∈ s ∪ t } := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False