Theorem: sb_injective (LeanCourse/MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean)

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
⊢ Injective (sbFun f g)
Tactic:
set A := sbSet f g with A_def
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
⊢ Injective (sbFun f g)

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
⊢ Injective (sbFun f g)
Tactic:
set h := sbFun f g with h_def
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
⊢ Injective h

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
⊢ Injective h
Tactic:
intro x₁ x₂
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
⊢ h x₁ = h x₂ → x₁ = x₂

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
⊢ h x₁ = h x₂ → x₁ = x₂
Tactic:
intro (hxeq : h x₁ = h x₂)
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂
Tactic:
simp only [h_def, sbFun, ← A_def] at hxeq
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
⊢ x₁ = x₂

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
⊢ x₁ = x₂
Tactic:
by_cases xA : x₁ ∈ A ∨ x₂ ∈ A
State after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
⊢ x₁ = x₂

case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : ¬(x₁ ∈ A ∨ x₂ ∈ A)
⊢ x₁ = x₂

State before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : ¬(x₁ ∈ A ∨ x₂ ∈ A)
⊢ x₁ = x₂
Tactic:
push_neg  at xA
State after:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂

State before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂
Tactic:
rw [if_neg xA.1, if_neg xA.2] at hxeq
State after:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : invFun g x₁ = invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂

State before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : invFun g x₁ = invFun g x₂
xA : x₁ ∉ A ∧ x₂ ∉ A
⊢ x₁ = x₂
Tactic:
rw [← sb_right_inv f g xA.1, hxeq, sb_right_inv f g xA.2]
State after:
no goals

State before:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
⊢ x₁ = x₂
Tactic:
wlog x₁A : x₁ ∈ A generalizing x₁ x₂ hxeq xA
State after:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₁ = x₂

α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₁ = x₂

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₁ = x₂
Tactic:
have x₂A : x₂ ∈ A := by
  apply not_imp_self.mp
  intro (x₂nA : x₂ ∉ A)
  rw [if_pos x₁A, if_neg x₂nA] at hxeq
  rw [A_def, sbSet, mem_iUnion] at x₁A
  have x₂eq : x₂ = g (f x₁) := by
    rw [hxeq, sb_right_inv f g x₂nA]
  rcases x₁A with ⟨n, hn⟩
  rw [A_def, sbSet, mem_iUnion]
  use n + 1
  simp [sbAux]
  exact ⟨x₁, hn, x₂eq.symm⟩
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂
Tactic:
rw [if_pos x₁A, if_pos x₂A] at hxeq
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = f x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = f x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂A : x₂ ∈ A
⊢ x₁ = x₂
Tactic:
exact hf hxeq
State after:
no goals

State before:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₁ = x₂
Tactic:
symm
State after:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₂ = x₁

State before:
case pos.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
this :
  ∀ ⦃x₁ x₂ : α⦄,
    ((if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂) → x₁ ∈ A ∨ x₂ ∈ A → x₁ ∈ A → x₁ = x₂
x₁A : x₁ ∉ A
⊢ x₂ = x₁
Tactic:
apply this hxeq.symm xA.symm (xA.resolve_left x₁A)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₂ ∈ A
Tactic:
apply not_imp_self.mp
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₂ ∉ A → x₂ ∈ A

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
⊢ x₂ ∉ A → x₂ ∈ A
Tactic:
intro (x₂nA : x₂ ∉ A)
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : (if x₁ ∈ A then f x₁ else invFun g x₁) = if x₂ ∈ A then f x₂ else invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
rw [if_pos x₁A, if_neg x₂nA] at hxeq
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
rw [A_def, sbSet, mem_iUnion] at x₁A
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
have x₂eq : x₂ = g (f x₁) := by
  rw [hxeq, sb_right_inv f g x₂nA]
State after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
⊢ x₂ ∈ A

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
⊢ x₂ ∈ A
Tactic:
rcases x₁A with ⟨n, hn⟩
State after:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ A

State before:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ A
Tactic:
rw [A_def, sbSet, mem_iUnion]
State after:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ i, x₂ ∈ sbAux f g i

State before:
case intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ i, x₂ ∈ sbAux f g i
Tactic:
use n + 1
State after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ sbAux f g (n + 1)

State before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ x₂ ∈ sbAux f g (n + 1)
Tactic:
simp [sbAux]
State after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ a ∈ sbAux f g n, g (f a) = x₂

State before:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sbAux f g n
⊢ ∃ a ∈ sbAux f g n, g (f a) = x₂
Tactic:
exact ⟨x₁, hn, x₂eq.symm⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
hg : Injective g
A : Set α := sbSet f g
A_def : A = sbSet f g
h : α → β := sbFun f g
h_def : h = sbFun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A ∨ x₂ ∈ A
x₁A : ∃ i, x₁ ∈ sbAux f g i
x₂nA : x₂ ∉ A
⊢ x₂ = g (f x₁)
Tactic:
rw [hxeq, sb_right_inv f g x₂nA]
State after:
no goals