Theorem: Set.update_id_injOn_iff (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 b : α
s : Set α
⊢ InjOn (update id a b) s ↔ a ∈ s → b ∈ s → a = b
Tactic:
rw [update_injOn_iff, and_iff_right injective_id.injOn]
State after:
α✝ : 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 b : α
s : Set α
⊢ (a ∈ s → ∀ x ∈ s, id x = b → x = a) ↔ a ∈ s → b ∈ s → a = b

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 b : α
s : Set α
⊢ (a ∈ s → ∀ x ∈ s, id x = b → x = a) ↔ a ∈ s → b ∈ s → a = b
Tactic:
refine ⟨fun h has hbs ↦ (h has b hbs rfl).symm, ?_⟩
State after:
α✝ : 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 b : α
s : Set α
⊢ (a ∈ s → b ∈ s → a = b) → a ∈ s → ∀ x ∈ s, id x = b → x = a

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 b : α
s : Set α
⊢ (a ∈ s → b ∈ s → a = b) → a ∈ s → ∀ x ∈ s, id x = b → x = a
Tactic:
rintro h has _ hbs rfl
State after:
α✝ : 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 : α
s : Set α
has : a ∈ s
x✝ : α
hbs : x✝ ∈ s
h : a ∈ s → id x✝ ∈ s → a = id x✝
⊢ x✝ = a

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 : α
s : Set α
has : a ∈ s
x✝ : α
hbs : x✝ ∈ s
h : a ∈ s → id x✝ ∈ s → a = id x✝
⊢ x✝ = a
Tactic:
exact (h has hbs).symm
State after:
no goals