Theorem: Set.update_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✝ : β
f : α → β
s : Set α
a : α
b : β
⊢ InjOn (update f a b) s ↔ InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
Tactic:
refine ⟨fun h ↦ ⟨fun x hx y hy hxy ↦  h hx.1 hy.1 ?_, ?_⟩, fun h x hx y hy hxy ↦ ?_⟩
State after:
case 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✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
x : α
hx : x ∈ s \ {a}
y : α
hy : y ∈ s \ {a}
hxy : f x = f y
⊢ update f a b x = update f a b y

case 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✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
⊢ a ∈ s → ∀ x ∈ s, f x = b → x = a

case 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✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
⊢ x = y

State before:
case 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✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
⊢ x = y
Tactic:
obtain (rfl | hxa) := eq_or_ne x a
State after:
case 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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
⊢ x = y

case refine_3.inr
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
⊢ x = y

State before:
case refine_3.inr
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
⊢ x = y
Tactic:
obtain (rfl | hya) := eq_or_ne y a
State after:
case refine_3.inr.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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : update f y b x = update f y b y
hxa : x ≠ y
⊢ x = y

case refine_3.inr.inr
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y

State before:
case refine_3.inr.inr
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y
Tactic:
rw [update_noteq hxa, update_noteq hya] at hxy
State after:
case refine_3.inr.inr
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x = f y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y

State before:
case refine_3.inr.inr
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x = f y
hxa : x ≠ a
hya : y ≠ a
⊢ x = y
Tactic:
exact h.1 ⟨hx, hxa⟩ ⟨hy, hya⟩ hxy
State after:
no goals

State before:
case 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✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
x : α
hx : x ∈ s \ {a}
y : α
hy : y ∈ s \ {a}
hxy : f x = f y
⊢ update f a b x = update f a b y
Tactic:
rwa [update_noteq hx.2, update_noteq hy.2]
State after:
no goals

State before:
case 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✝ : β
f : α → β
s : Set α
a : α
b : β
h : InjOn (update f a b) s
⊢ a ∈ s → ∀ x ∈ s, f x = b → x = a
Tactic:
rintro has x hxs rfl
State after:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
⊢ x = a

State before:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
⊢ x = a
Tactic:
by_contra! hne
State after:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
⊢ False

State before:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
⊢ False
Tactic:
have h' := h hxs has
State after:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : update f a (f x) x = update f a (f x) a → x = a
⊢ False

State before:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : update f a (f x) x = update f a (f x) a → x = a
⊢ False
Tactic:
rw [update_noteq hne, update_same] at h'
State after:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : f x = f x → x = a
⊢ False

State before:
case 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 : β
f : α → β
s : Set α
a : α
has : a ∈ s
x : α
hxs : x ∈ s
h : InjOn (update f a (f x)) s
hne : x ≠ a
h' : f x = f x → x = a
⊢ False
Tactic:
exact hne <| h' rfl
State after:
no goals

State before:
case 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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
⊢ x = y
Tactic:
by_contra! hne
State after:
case 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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
hne : x ≠ y
⊢ False

State before:
case 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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : update f x b x = update f x b y
hne : x ≠ y
⊢ False
Tactic:
rw [update_same, update_noteq hne.symm] at hxy
State after:
case 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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : b = f y
hne : x ≠ y
⊢ False

State before:
case 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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : b = f y
hne : x ≠ y
⊢ False
Tactic:
exact hne.symm <| h.2 hx y hy hxy.symm
State after:
no goals

State before:
case refine_3.inr.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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : update f y b x = update f y b y
hxa : x ≠ y
⊢ x = y
Tactic:
rw [update_noteq hxa, update_same] at hxy
State after:
case refine_3.inr.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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : f x = b
hxa : x ≠ y
⊢ x = y

State before:
case refine_3.inr.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✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {y}) ∧ (y ∈ s → ∀ x ∈ s, f x = b → x = y)
hxy : f x = b
hxa : x ≠ y
⊢ x = y
Tactic:
exact h.2 hy x hx hxy
State after:
no goals