Theorem: sb_surjective (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 : β → α
hg : Injective g
⊢ Surjective (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 : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
⊢ Surjective (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 : β → α
hg : Injective g
A : Set α := sb_set f g
A_def : A = sb_set f g
⊢ Surjective (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 : β → α
hg : Injective g
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
⊢ Surjective 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 : β → α
hg : Injective g
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
⊢ Surjective h
Tactic:
intro y
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 : β → α
hg : Injective g
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
y : β
⊢ ∃ a, h a = y

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 : β → α
hg : Injective g
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
y : β
⊢ ∃ a, h a = y
Tactic:
by_cases gyA : g y ∈ 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 : β → α
hg : Injective g
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
y : β
gyA : g y ∈ A
⊢ ∃ a, h a = y

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 : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ ∃ a, h a = y

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 : β → α
hg : Injective g
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
y : β
gyA : g y ∈ A
⊢ ∃ a, h a = y
Tactic:
rw [A_def, sb_set, mem_iUnion] at gyA
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 : β → α
hg : Injective g
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
y : β
gyA : ∃ i, g y ∈ sb_aux f g i
⊢ ∃ a, h a = y

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 : β → α
hg : Injective g
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
y : β
gyA : ∃ i, g y ∈ sb_aux f g i
⊢ ∃ a, h a = y
Tactic:
rcases gyA with ⟨n, hn⟩
State after:
case pos.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 : β → α
hg : Injective g
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
y : β
n : ℕ
hn : g y ∈ sb_aux f g n
⊢ ∃ a, h a = y

State before:
case pos.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 : β → α
hg : Injective g
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
y : β
n : ℕ
hn : g y ∈ sb_aux f g n
⊢ ∃ a, h a = y
Tactic:
cases n with
| zero =>
  simp [sb_aux] at hn
| succ n =>
  simp [sb_aux] at hn
  rcases hn with ⟨x, xmem, hx⟩
  use x
  have : x ∈ A := by
    rw [A_def, sb_set, mem_iUnion]
    exact ⟨n, xmem⟩
  simp only [h_def, sb_fun, if_pos this]
  exact hg hx
State after:
no goals

State before:
case pos.intro.zero
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
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
y : β
hn : g y ∈ sb_aux f g Nat.zero
⊢ ∃ a, h a = y
Tactic:
simp [sb_aux] at hn
State after:
no goals

State before:
case pos.intro.succ
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
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
y : β
n : ℕ
hn : g y ∈ sb_aux f g (Nat.succ n)
⊢ ∃ a, h a = y
Tactic:
simp [sb_aux] at hn
State after:
case pos.intro.succ
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
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
y : β
n : ℕ
hn : ∃ a ∈ sb_aux f g n, g (f a) = g y
⊢ ∃ a, h a = y

State before:
case pos.intro.succ
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
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
y : β
n : ℕ
hn : ∃ a ∈ sb_aux f g n, g (f a) = g y
⊢ ∃ a, h a = y
Tactic:
rcases hn with ⟨x, xmem, hx⟩
State after:
case pos.intro.succ.intro.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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ a, h a = y

State before:
case pos.intro.succ.intro.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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ a, h a = y
Tactic:
use x
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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ h x = y

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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ h x = y
Tactic:
have : x ∈ A := by
  rw [A_def, sb_set, mem_iUnion]
  exact ⟨n, xmem⟩
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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y

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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ h x = y
Tactic:
simp only [h_def, sb_fun, if_pos this]
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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ f x = y

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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
this : x ∈ A
⊢ f x = y
Tactic:
exact hg hx
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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ x ∈ A
Tactic:
rw [A_def, sb_set, mem_iUnion]
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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ i, x ∈ sb_aux f g i

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 : β → α
hg : Injective g
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
y : β
n : ℕ
x : α
xmem : x ∈ sb_aux f g n
hx : g (f x) = g y
⊢ ∃ i, x ∈ sb_aux f g i
Tactic:
exact ⟨n, xmem⟩
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 : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ ∃ a, h a = y
Tactic:
use g y
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 : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ h (g y) = y

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 : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ h (g y) = y
Tactic:
simp [sb_fun, gyA]
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 : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ invFun g (g y) = y

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 : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ invFun g (g y) = y
Tactic:
apply hg
State after:
case h.a
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ g (invFun g (g y)) = g y

State before:
case h.a
α✝ : Type u_1
β✝ : Type u_2
inst✝¹ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
β : Type u_4
inst✝ : Nonempty β
f : α → β
g : β → α
hg : Injective g
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
y : β
gyA : g y ∉ A
⊢ g (invFun g (g y)) = g y
Tactic:
exact apply_invFun_apply
State after:
no goals