Theorem: sb_injective (LeanTeaching/TD/TD06.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
⊢ Injective (sb_fun f g)
Tactic:
set A := sb_set f g with A_def
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
⊢ Injective (sb_fun f g)

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
⊢ Injective (sb_fun f g)
Tactic:
set h := sb_fun f g with h_def
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
⊢ Injective h

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
⊢ Injective h
Tactic:
intro x₁ x₂ hxeq
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : h x₁ = h x₂
⊢ x₁ = x₂
Tactic:
simp only [h_def, sb_fun, ←A_def] at hxeq
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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 pos
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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:
rcases xA with (xA | xA)
State after:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂

case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂

State before:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Tactic:
have x₂A : x₂ ∈ A := by
  apply not_imp_self.mp
  intro x₂nA
  rw [if_pos xA, if_neg x₂nA] at hxeq
  rw [A_def, sb_set, mem_iUnion] at xA
  have x₂eq : x₂ = g (f x₁) := by
    rw [← sb_right_inv f g x₂nA, hxeq]
  rcases xA with ⟨n, hn⟩
  rw [A_def, sb_set, mem_iUnion]
  use n + 1
  simp [sb_aux]
  exact ⟨x₁, hn, x₂eq.symm⟩
State after:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂

State before:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Tactic:
simp [xA, x₂A] at hxeq
State after:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₁ ∈ A
x₂A : x₂ ∈ A
hxeq : f x₁ = f x₂
⊢ x₁ = x₂

State before:
case pos.inl
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₁ ∈ A
x₂A : x₂ ∈ A
hxeq : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
exact hf hxeq
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Tactic:
apply not_imp_self.mp
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Tactic:
intro x₂nA
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂nA : x₂ ∉ A
⊢ x₂ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
rw [if_pos xA, if_neg x₂nA] at hxeq
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : x₁ ∈ A
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
rw [A_def, sb_set, mem_iUnion] at xA
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : ∃ i, x₁ ∈ sb_aux f g i
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : ∃ i, x₁ ∈ sb_aux f g i
x₂nA : x₂ ∉ A
⊢ x₂ ∈ A
Tactic:
have x₂eq : x₂ = g (f x₁) := by
  rw [← sb_right_inv f g x₂nA, hxeq]
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : ∃ i, x₁ ∈ sb_aux f g i
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
⊢ x₂ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : ∃ i, x₁ ∈ sb_aux f g i
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
⊢ x₂ ∈ A
Tactic:
rcases xA with ⟨n, hn⟩
State after:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ x₂ ∈ A

State before:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ x₂ ∈ A
Tactic:
rw [A_def, sb_set, mem_iUnion]
State after:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ ∃ i, x₂ ∈ sb_aux f g i

State before:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ ∃ i, x₂ ∈ sb_aux f g i
Tactic:
use n + 1
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ x₂ ∈ sb_aux f g (n + 1)

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ x₂ ∈ sb_aux f g (n + 1)
Tactic:
simp [sb_aux]
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ ∃ a ∈ sb_aux f g n, g (f a) = x₂

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
x₂nA : x₂ ∉ A
x₂eq : x₂ = g (f x₁)
n : ℕ
hn : x₁ ∈ sb_aux f g n
⊢ ∃ a ∈ sb_aux 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : f x₁ = invFun g x₂
xA : ∃ i, x₁ ∈ sb_aux f g i
x₂nA : x₂ ∉ A
⊢ x₂ = g (f x₁)
Tactic:
rw [← sb_right_inv f g x₂nA, hxeq]
State after:
no goals

State before:
case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Tactic:
have x₁A : x₁ ∈ A := by
  apply not_imp_self.mp
  intro x₁nA
  rw [if_pos xA, if_neg x₁nA] at hxeq
  rw [A_def, sb_set, mem_iUnion] at xA
  have x₁eq : x₁ = g (f x₂) := by
    rw [← sb_right_inv f g x₁nA, hxeq]
  rcases xA with ⟨n, hn⟩
  rw [A_def, sb_set, mem_iUnion]
  use n + 1
  simp [sb_aux]
  exact ⟨x₂, hn, x₁eq.symm⟩
State after:
case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂

State before:
case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁ = x₂
Tactic:
simp [xA, x₁A] at hxeq
State after:
case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₂ ∈ A
x₁A : x₁ ∈ A
hxeq : f x₁ = f x₂
⊢ x₁ = x₂

State before:
case pos.inr
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₂ ∈ A
x₁A : x₁ ∈ A
hxeq : f x₁ = f x₂
⊢ x₁ = x₂
Tactic:
exact hf hxeq
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Tactic:
apply not_imp_self.mp
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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
Tactic:
intro x₁nA
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁nA : x₁ ∉ A
⊢ x₁ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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₁nA : x₁ ∉ A
⊢ x₁ ∈ A
Tactic:
rw [if_pos xA, if_neg x₁nA] at hxeq
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : x₂ ∈ A
x₁nA : x₁ ∉ A
⊢ x₁ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : x₂ ∈ A
x₁nA : x₁ ∉ A
⊢ x₁ ∈ A
Tactic:
rw [A_def, sb_set, mem_iUnion] at xA
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : ∃ i, x₂ ∈ sb_aux f g i
x₁nA : x₁ ∉ A
⊢ x₁ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : ∃ i, x₂ ∈ sb_aux f g i
x₁nA : x₁ ∉ A
⊢ x₁ ∈ A
Tactic:
have x₁eq : x₁ = g (f x₂) := by
  rw [← sb_right_inv f g x₁nA, hxeq]
State after:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : ∃ i, x₂ ∈ sb_aux f g i
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
⊢ x₁ ∈ A

State before:
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : ∃ i, x₂ ∈ sb_aux f g i
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
⊢ x₁ ∈ A
Tactic:
rcases xA with ⟨n, hn⟩
State after:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ x₁ ∈ A

State before:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ x₁ ∈ A
Tactic:
rw [A_def, sb_set, mem_iUnion]
State after:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ ∃ i, x₁ ∈ sb_aux f g i

State before:
case intro
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ ∃ i, x₁ ∈ sb_aux f g i
Tactic:
use n + 1
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ x₁ ∈ sb_aux f g (n + 1)

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ x₁ ∈ sb_aux f g (n + 1)
Tactic:
simp [sb_aux]
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ ∃ a ∈ sb_aux f g n, g (f a) = x₁

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
x₁nA : x₁ ∉ A
x₁eq : x₁ = g (f x₂)
n : ℕ
hn : x₂ ∈ sb_aux f g n
⊢ ∃ a ∈ sb_aux 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
hxeq : invFun g x₁ = f x₂
xA : ∃ i, x₂ ∈ sb_aux f g i
x₁nA : x₁ ∉ A
⊢ x₁ = g (f x₂)
Tactic:
rw [← sb_right_inv f g x₁nA, hxeq]
State after:
no goals

State before:
case neg
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun 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:
simp [xA] at hxeq
State after:
case neg
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₁ ∉ A ∧ x₂ ∉ A
hxeq : invFun g x₁ = invFun g x₂
⊢ x₁ = x₂

State before:
case neg
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
A : Set α := sb_set f g
A_def : A = sb_set f g
h : α → β := sb_fun f g
h_def : h = sb_fun f g
x₁ x₂ : α
xA : x₁ ∉ A ∧ x₂ ∉ A
hxeq : invFun g x₁ = invFun g x₂
⊢ x₁ = x₂
Tactic:
rw [← sb_right_inv f g xA.1, ← sb_right_inv f g xA.2, hxeq]
State after:
no goals