Theorem: Set.preimage_update_of_not_mem_not_mem (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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
⊢ update f a b ⁻¹' s = f ⁻¹' s
Tactic:
ext x
State after:
case h
α✝ : 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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s

State before:
case h
α✝ : 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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ f ⁻¹' s
Tactic:
simp only [mem_preimage, update_apply]
State after:
case h
α✝ : 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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ (if x = a then b else f x) ∈ s ↔ f x ∈ s

State before:
case h
α✝ : 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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
⊢ (if x = a then b else f x) ∈ s ↔ f x ∈ s
Tactic:
split_ifs with h
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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : x = a
⊢ b ∈ s ↔ f x ∈ s

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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s

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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : x = a
⊢ b ∈ s ↔ f x ∈ s

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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s
Tactic:
simp [hbs, h.symm ▸ has]
State after:
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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ 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 : α → β
s : Set β
hbs : b ∉ s
has : f a ∉ s
x : α
h : ¬x = a
⊢ f x ∈ s ↔ f x ∈ s
Tactic:
rfl
State after:
no goals