Theorem: sb_right_inv (MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean)

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
⊢ g (invFun g x) = x
Tactic:
have : x ∈ g '' univ := by
  contrapose! hx
  rw [sbSet, mem_iUnion]
  use 0
  rw [sbAux, mem_diff]
  exact ⟨mem_univ _, hx⟩
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : x ∈ g '' univ
⊢ g (invFun g x) = x
Tactic:
have : ∃ y, g y = x := by
  simp at this
  assumption
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this✝ : x ∈ g '' univ
this : ∃ y, g y = x
⊢ g (invFun g x) = x

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this✝ : x ∈ g '' univ
this : ∃ y, g y = x
⊢ g (invFun g x) = x
Tactic:
exact invFun_eq this
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
⊢ x ∈ g '' univ
Tactic:
contrapose! hx
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbSet f g

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbSet f g
Tactic:
rw [sbSet, mem_iUnion]
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sbAux f g i

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sbAux f g i
Tactic:
use 0
State after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbAux f g 0

State before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbAux f g 0
Tactic:
rw [sbAux, mem_diff]
State after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ univ ∧ x ∉ g '' univ

State before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ univ ∧ x ∉ g '' univ
Tactic:
exact ⟨mem_univ _, hx⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : x ∈ g '' univ
⊢ ∃ y, g y = x
Tactic:
simp at this
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : ∃ y, g y = x
⊢ ∃ y, g y = x

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ sbSet f g
this : ∃ y, g y = x
⊢ ∃ y, g y = x
Tactic:
assumption
State after:
no goals