α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f a = b
rw [hpi, dif_pos h'] at h
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b
injection h with h
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b
subst h
no goals
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b
apply Classical.choose_spec h'
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
rw [hpi, dif_neg h'] at h
no goals
α✝ : Sort ?u.12530
β✝ : Sort ?u.12533
γ : Sort ?u.12536
f✝ : α✝ → β✝
α : Type u_1
β : Sort u_2
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
contradiction