Theorem: Set.update_injective (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 : β
hf : Injective f
a : α
h : b ∉ range f
⊢ Injective (update f a b)
Tactic:
rintro x y hy
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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : update f a b x = update f a b y
⊢ x = y

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : update f a b x = update f a b y
⊢ x = y
Tactic:
rw [update_apply, update_apply] at hy
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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : (if x = a then b else f x) = if y = a then b else f y
⊢ x = y

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
hy : (if x = a then b else f x) = if y = a then b else f y
⊢ x = y
Tactic:
split_ifs at hy with h_1 h_2
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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : y = a
hy : b = b
⊢ x = y

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : ¬y = a
hy : b = f y
⊢ x = y

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : y = a
hy : f x = b
⊢ x = y

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : ¬y = a
hy : f x = f y
⊢ x = y

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : ¬y = a
hy : f x = f y
⊢ x = y
Tactic:
exact hf.eq_iff.1 hy
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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : y = a
hy : b = b
⊢ x = y
Tactic:
rw [h_1,h_2]
State after:
no goals

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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : x = a
h_2 : ¬y = a
hy : b = f y
⊢ x = y
Tactic:
exact (h ⟨y, hy.symm⟩).elim
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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : y = a
hy : f x = b
⊢ x = y
Tactic:
exact (h ⟨x, hy⟩).elim
State after:
no goals