Theorem: Set.preimage_update_eq_ite (Matroid/ForMathlib/Function.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
⊢ update f a b ⁻¹' s = if b ∈ s then insert a (f ⁻¹' s) else if f a ∈ s then f ⁻¹' s \ {a} else f ⁻¹' s
Tactic:
split_ifs with hb ha
State after:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∈ s
⊢ update f a b ⁻¹' s = insert a (f ⁻¹' s)

case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∈ s
⊢ update f a b ⁻¹' s = f ⁻¹' s \ {a}

case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∉ s
⊢ update f a b ⁻¹' s = f ⁻¹' s

State before:
case neg
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∉ s
⊢ update f a b ⁻¹' s = f ⁻¹' s
Tactic:
rw [preimage_update_of_not_mem_not_mem _ hb ha]
State after:
no goals

State before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∈ s
⊢ update f a b ⁻¹' s = insert a (f ⁻¹' s)
Tactic:
rw [preimage_update_of_mem _ hb]
State after:
no goals

State before:
case pos
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
f✝ : α → β
a✝ : α
b✝ : β
f : α → β
a : α
b : β
s : Set β
inst✝¹ : Decidable (b ∈ s)
inst✝ : Decidable (f a ∈ s)
hb : b ∉ s
ha : f a ∈ s
⊢ update f a b ⁻¹' s = f ⁻¹' s \ {a}
Tactic:
rw [preimage_update_of_not_mem_mem _ hb ha]
State after:
no goals