α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
intros
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h this : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
have := h
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h this : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
cases' this with g
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
let h : α ≃ β :=
  (Set.sumCompl (s : Set α)).symm.trans
    ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
⊢ ∀ (x : ↑s), ↑h ↑x = ↑f x
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
refine' ⟨h, _⟩
case intro.mk
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
x : α
hx : x ∈ s
⊢ ↑h ↑{ val := x, property := hx } = ↑f { val := x, property := hx }
case intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
⊢ ∀ (x : ↑s), ↑h ↑x = ↑f x
rintro ⟨x, hx⟩
no goals
case intro.mk
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
g : ↑(sᶜ) ≃ ↑(range ↑fᶜ)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans ((sumCongr (ofInjective ↑f (_ : Injective f.toFun)) g).trans (Set.sumCompl (range ↑f)))
x : α
hx : x ∈ s
⊢ ↑h ↑{ val := x, property := hx } = ↑f { val := x, property := hx }
simp [Set.sumCompl_symm_apply_of_mem, hx]