Theorem: Set.image_update (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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
⊢ update f a b '' s = if a ∈ s then insert b (f '' (s \ {a})) else f '' 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ update f a b '' s = insert b (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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ update f a b '' s = f '' s
Tactic:
rw [subset_antisymm_iff, image_subset_iff, image_subset_iff]
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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ s ⊆ update f a b ⁻¹' (f '' s) ∧ s ⊆ f ⁻¹' (update f a b '' 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
⊢ s ⊆ update f a b ⁻¹' (f '' s) ∧ s ⊆ f ⁻¹' (update f a b '' s)
Tactic:
refine ⟨fun x hxs ↦ ⟨x, hxs, ?_⟩, fun x hxs ↦ ⟨x, hxs, ?_⟩⟩
State after:
case neg.refine_1
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ f x = update f a b x

case neg.refine_2
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ update f a b x = f x

State before:
case neg.refine_2
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ update f a b x = f x
Tactic:
rw [update_noteq]
State after:
case neg.refine_2.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a

State before:
case neg.refine_2.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a
Tactic:
rintro rfl
State after:
case neg.refine_2.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 α
b : β
x : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False

State before:
case neg.refine_2.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 α
b : β
x : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False
Tactic:
exact h hxs
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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ update f a b '' s = insert b (f '' (s \ {a}))
Tactic:
rw [subset_antisymm_iff, image_subset_iff]
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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ s ⊆ update f a b ⁻¹' insert b (f '' (s \ {a})) ∧ insert b (f '' (s \ {a})) ⊆ update f a b '' 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
⊢ s ⊆ update f a b ⁻¹' insert b (f '' (s \ {a})) ∧ insert b (f '' (s \ {a})) ⊆ update f a b '' s
Tactic:
refine ⟨fun x hxs ↦ (em (x = a)).elim (fun heq ↦ ?_) (fun hne ↦ Or.inr ?_), fun x ↦ ?_⟩
State after:
case pos.refine_1
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ x ∈ update f a b ⁻¹' insert b (f '' (s \ {a}))

case pos.refine_2
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
hne : ¬x = a
⊢ update f a b x ∈ f '' (s \ {a})

case pos.refine_3
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : β
⊢ x ∈ insert b (f '' (s \ {a})) → x ∈ update f a b '' s

State before:
case pos.refine_3
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : β
⊢ x ∈ insert b (f '' (s \ {a})) → x ∈ update f a b '' s
Tactic:
rintro (rfl | ⟨x, hx, rfl⟩)
State after:
case pos.refine_3.inl
α✝ : 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 : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ x ∈ update f a x '' s

case pos.refine_3.inr.intro.intro
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hx : x ∈ s \ {a}
⊢ f x ∈ update f a b '' s

State before:
case pos.refine_3.inr.intro.intro
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hx : x ∈ s \ {a}
⊢ f x ∈ update f a b '' s
Tactic:
exact ⟨x, hx.1, update_noteq hx.2 _ _⟩
State after:
no goals

State before:
case pos.refine_1
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ x ∈ update f a b ⁻¹' insert b (f '' (s \ {a}))
Tactic:
rw [mem_preimage, update_apply, if_pos heq]
State after:
case pos.refine_1
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ b ∈ insert b (f '' (s \ {a}))

State before:
case pos.refine_1
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
heq : x = a
⊢ b ∈ insert b (f '' (s \ {a}))
Tactic:
exact mem_insert _ _
State after:
no goals

State before:
case pos.refine_2
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
hne : ¬x = a
⊢ update f a b x ∈ f '' (s \ {a})
Tactic:
exact ⟨x, ⟨hxs, hne⟩, by rw [update_noteq hne]⟩
State after:
no goals

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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∈ s
x : α
hxs : x ∈ s
hne : ¬x = a
⊢ f x = update f a b x
Tactic:
rw [update_noteq hne]
State after:
no goals

State before:
case pos.refine_3.inl
α✝ : 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 : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ x ∈ update f a x '' s
Tactic:
use a
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 : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ a ∈ s ∧ update f a x a = x

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 : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
h : a ∈ s
x : β
⊢ a ∈ s ∧ update f a x a = x
Tactic:
simpa
State after:
no goals

State before:
case neg.refine_1
α✝ : 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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ f x = update f a b x
Tactic:
rw [update_noteq]
State after:
case neg.refine_1.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a

State before:
case neg.refine_1.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✝ : β
a : α
f : α → β
s : Set α
inst✝ : Decidable (a ∈ s)
b : β
h : a ∉ s
x : α
hxs : x ∈ s
⊢ x ≠ a
Tactic:
rintro rfl
State after:
case neg.refine_1.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 α
b : β
x : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False

State before:
case neg.refine_1.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 α
b : β
x : α
hxs : x ∈ s
inst✝ : Decidable (x ∈ s)
h : x ∉ s
⊢ False
Tactic:
exact h hxs
State after:
no goals