-- Mathlib/Logic/Function/Basic.lean
lemma Injective.dite (p : α → Prop) [DecidablePred p]
    {f : {a : α // p a} → β} {f' : {a : α // ¬ p a} → β}
    (hf : Injective f) (hf' : Injective f')
    (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬ p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩) :
    Function.Injective (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) := fun x₁ x₂ h => by
 dsimp only at h
 by_cases h₁ : p x₁ <;> by_cases h₂ : p x₂
 · rw [dif_pos h₁, dif_pos h₂] at h; injection (hf h)
 · rw [dif_pos h₁, dif_neg h₂] at h; exact (im_disj h).elim
 · rw [dif_neg h₁, dif_pos h₂] at h; exact (im_disj h.symm).elim
 · rw [dif_neg h₁, dif_neg h₂] at h; injection (hf' h)

Proof state:
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
⊢ x₁ = x₂

Tactic:
by_cases h₁ : p x₁ <;> by_cases h₂ : p x₂

Result:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : p x₁
h₂ : p x₂
⊢ x₁ = x₂

case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂

case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : ¬p x₁
h₂ : p x₂
⊢ x₁ = x₂

case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : ¬p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂

Proof state:
case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : p x₁
h₂ : ¬p x₂
h : f ⟨x₁, h₁⟩ = f' ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
exact (im_disj h).elim

Result:
no goals

Proof state:
case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : ¬p x₂
h : f' ⟨x₁, h₁⟩ = f' ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
injection (hf' h)

Result:
no goals

Proof state:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : p x₁
h₂ : p x₂
⊢ x₁ = x₂

Tactic:
rw [dif_pos h₁, dif_pos h₂] at h

Result:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : p x₁
h₂ : p x₂
h : f ⟨x₁, h₁⟩ = f ⟨x₂, h₂⟩
⊢ x₁ = x₂

Proof state:
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (fun x => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₁ = (fun x => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₂
⊢ x₁ = x₂

Tactic:
dsimp only at h

Result:
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
⊢ x₁ = x₂

Proof state:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : p x₁
h₂ : p x₂
h : f ⟨x₁, h₁⟩ = f ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
injection (hf h)

Result:
no goals

Proof state:
case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂

Tactic:
rw [dif_pos h₁, dif_neg h₂] at h

Result:
case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : p x₁
h₂ : ¬p x₂
h : f ⟨x₁, h₁⟩ = f' ⟨x₂, h₂⟩
⊢ x₁ = x₂

Proof state:
case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : ¬p x₁
h₂ : ¬p x₂
⊢ x₁ = x₂

Tactic:
rw [dif_neg h₁, dif_neg h₂] at h

Result:
case neg
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : ¬p x₂
h : f' ⟨x₁, h₁⟩ = f' ⟨x₂, h₂⟩
⊢ x₁ = x₂

Proof state:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : p x₂
h : f' ⟨x₁, h₁⟩ = f ⟨x₂, h₂⟩
⊢ x₁ = x₂

Tactic:
exact (im_disj h.symm).elim

Result:
no goals

Proof state:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (if h : p x₁ then f ⟨x₁, h⟩ else f' ⟨x₁, h⟩) = if h : p x₂ then f ⟨x₂, h⟩ else f' ⟨x₂, h⟩
h₁ : ¬p x₁
h₂ : p x₂
⊢ x₁ = x₂

Tactic:
rw [dif_neg h₁, dif_pos h₂] at h

Result:
case pos
α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h₁ : ¬p x₁
h₂ : p x₂
h : f' ⟨x₁, h₁⟩ = f ⟨x₂, h₂⟩
⊢ x₁ = x₂