Theorem: Equiv.swap_image_eq_exchange (Matroid/ForMathlib/Other.lean)

State before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
⊢ ⇑(swap e f) '' S = insert f (S \ {e})
Tactic:
ext x
State after:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ insert f (S \ {e})

State before:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ x ∈ ⇑(swap e f) '' S ↔ x ∈ insert f (S \ {e})
Tactic:
rw [image_equiv_eq_preimage_symm, mem_preimage, Equiv.symm_swap, Equiv.swap_apply_def,
  mem_insert_iff, mem_diff]
State after:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ (if x = e then f else if x = f then e else x) ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}

State before:
case h
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
⊢ (if x = e then f else if x = f then e else x) ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
split_ifs with hxe hxf
State after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : x = e
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}

case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : x = f
⊢ e ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}

case neg
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : ¬x = f
⊢ x ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}

State before:
case neg
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : ¬x = f
⊢ x ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
simp [hxe, iff_false_intro hxf]
State after:
no goals

State before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : x = e
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
subst hxe
State after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {x}

State before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ f ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {x}
Tactic:
simp [he, hf, (show x ≠ f by rintro rfl; exact hf he)]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ x ≠ f
Tactic:
rintro rfl
State after:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
inst✝ : DecidableEq α
S : Set α
x : α
he : x ∈ S
hf : x ∉ S
⊢ False

State before:
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
inst✝ : DecidableEq α
S : Set α
x : α
he : x ∈ S
hf : x ∉ S
⊢ False
Tactic:
exact hf he
State after:
no goals

State before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
e f : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
hf : f ∉ S
x : α
hxe : ¬x = e
hxf : x = f
⊢ e ∈ S ↔ x = f ∨ x ∈ S ∧ x ∉ {e}
Tactic:
subst hxf
State after:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
e : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
x : α
hxe : ¬x = e
hf : x ∉ S
⊢ e ∈ S ↔ x = x ∨ x ∈ S ∧ x ∉ {e}

State before:
case pos
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
e : α
inst✝ : DecidableEq α
S : Set α
he : e ∈ S
x : α
hxe : ¬x = e
hf : x ∉ S
⊢ e ∈ S ↔ x = x ∨ x ∈ S ∧ x ∉ {e}
Tactic:
simp [he]
State after:
no goals