internlm/Lean-Github huggingface dataset:
Theorem: step_west
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x,y⟩ w = make_move ⟨s,⟨x+1, y⟩,w⟩ Move.west :=
         by have h' : x + 1 - 1 = x := rfl
            simp [h', hclear']
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Theorem: step_west
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Tactic:
rw [hmm] at W
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable (make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Theorem: step_west
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable (make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
⊢ Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
Tactic:
exact .Step ⟨s,⟨x+1,y⟩,w⟩ Move.west W
Proof state after:
no goals
Theorem: step_west
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
Tactic:
have h' : x + 1 - 1 = x := rfl
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : x + 1 - 1 = x
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
Theorem: step_west
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
W : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : x + 1 - 1 = x
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x + 1, y := y }, walls := w } Move.west
Tactic:
simp [h', hclear']
Proof state after:
no goals
Theorem: step_east
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x + 1, y := y } w = true
hinbounds : x + 1 ≤ s.x
E : Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x+1,y⟩ w = make_move ⟨s, ⟨x,y⟩,w⟩ Move.east :=
  by simp [hclear', hinbounds]
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x + 1, y := y } w = true
hinbounds : x + 1 ≤ s.x
E : Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
hmm :
  { size := s, position := { x := x + 1, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.east
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Theorem: step_east
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x + 1, y := y } w = true
hinbounds : x + 1 ≤ s.x
E : Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
hmm :
  { size := s, position := { x := x + 1, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.east
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
rw [hmm] at E
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x + 1, y := y } w = true
hinbounds : x + 1 ≤ s.x
E : Escapable (make_move { size := s, position := { x := x, y := y }, walls := w } Move.east)
hmm :
  { size := s, position := { x := x + 1, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.east
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Theorem: step_east
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x + 1, y := y } w = true
hinbounds : x + 1 ≤ s.x
E : Escapable (make_move { size := s, position := { x := x, y := y }, walls := w } Move.east)
hmm :
  { size := s, position := { x := x + 1, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.east
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
exact .Step ⟨s, ⟨x,y⟩, w⟩ Move.east E
Proof state after:
no goals
Theorem: step_east
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x + 1, y := y } w = true
hinbounds : x + 1 ≤ s.x
E : Escapable { size := s, position := { x := x + 1, y := y }, walls := w }
⊢ { size := s, position := { x := x + 1, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.east
Tactic:
simp [hclear', hinbounds]
Proof state after:
no goals
Theorem: step_north
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x,y⟩ w = make_move ⟨s,⟨x, y+1⟩,w⟩ Move.north :=
  by have h' : y + 1 - 1 = y := rfl
     simp [h', hclear']
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Theorem: step_north
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Tactic:
rw [hmm] at N
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable (make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Theorem: step_north
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable (make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north)
hmm :
  { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
⊢ Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
Tactic:
exact .Step ⟨s,⟨x,y+1⟩,w⟩ Move.north N
Proof state after:
no goals
Theorem: step_north
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
Tactic:
have h' : y + 1 - 1 = y := rfl
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : y + 1 - 1 = y
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
Theorem: step_north
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y } w = true
N : Escapable { size := s, position := { x := x, y := y }, walls := w }
h' : y + 1 - 1 = y
⊢ { size := s, position := { x := x, y := y }, walls := w } =
    make_move { size := s, position := { x := x, y := y + 1 }, walls := w } Move.north
Tactic:
simp [h', hclear']
Proof state after:
no goals
Theorem: step_south
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
have hmm : GameState.mk s ⟨x,y+1⟩ w = make_move ⟨s,⟨x, y⟩,w⟩ Move.south :=
     by simp [hclear', hinbounds]
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Theorem: step_south
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
rw [hmm] at S
Proof state after:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable (make_move { size := s, position := { x := x, y := y }, walls := w } Move.south)
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Theorem: step_south
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable (make_move { size := s, position := { x := x, y := y }, walls := w } Move.south)
hmm :
  { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
⊢ Escapable { size := s, position := { x := x, y := y }, walls := w }
Tactic:
exact .Step ⟨s,⟨x,y⟩,w⟩ Move.south S
Proof state after:
no goals
Theorem: step_south
Proof state before:
s : Coords
x y : Nat
w : List Coords
hclear' : List.notElem { x := x, y := y + 1 } w = true
hinbounds : y + 1 ≤ s.y
S : Escapable { size := s, position := { x := x, y := y + 1 }, walls := w }
⊢ { size := s, position := { x := x, y := y + 1 }, walls := w } =
    make_move { size := s, position := { x := x, y := y }, walls := w } Move.south
Tactic:
simp [hclear', hinbounds]
Proof state after:
no goals
Theorem: sb_right_inv
Proof 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]
  sorry
Proof 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
Theorem: sb_right_inv
Proof 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
  sorry
Proof 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
Theorem: sb_right_inv
Proof 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:
sorry
Proof state after:
no goals
Theorem: sb_right_inv
Proof 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:
sorry
Proof state after:
no goals
Theorem: sb_right_inv
Proof 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:
sorry
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
sorry
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
    sorry
  rcases x₁A with ⟨n, hn⟩
  rw [A_def, sbSet, mem_iUnion]
  use n + 1
  simp [sbAux]
  exact ⟨x₁, hn, x₂eq.symm⟩
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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₂
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
sorry
Proof state after:
no goals
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
  sorry
Proof state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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
Theorem: sb_injective
Proof state before:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
hf : Injective f
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:
sorry
Proof state after:
no goals
Theorem: sb_surjective
Proof 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
y : β
gyA : g y ∉ A
⊢ ∃ a, h a = y
Tactic:
sorry
Proof state after:
no goals
Theorem: sb_surjective
Proof state before:
case pos.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
y : β
n : ℕ
hn : g y ∈ sbAux f g n
⊢ ∃ a, h a = y
Tactic:
rcases n with _ | n
Proof state after:
case pos.intro.zero
α : 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
y : β
hn : g y ∈ sbAux f g Nat.zero
⊢ ∃ a, h a = y

case pos.intro.succ
α : 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
y : β
n : ℕ
hn : g y ∈ sbAux f g (Nat.succ n)
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.succ
α : 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
y : β
n : ℕ
hn : g y ∈ sbAux f g (Nat.succ n)
⊢ ∃ a, h a = y
Tactic:
simp [sbAux] at hn
Proof state after:
case pos.intro.succ
α : 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
y : β
n : ℕ
hn : ∃ a ∈ sbAux f g n, g (f a) = g y
⊢ ∃ a, h a = y
Theorem: sb_surjective
Proof state before:
case pos.intro.zero
α : 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
y : β
hn : g y ∈ sbAux f g Nat.zero
⊢ ∃ a, h a = y
Tactic:
simp [sbAux] at hn
Proof state after:
no goals
Theorem: aux
Proof state before:
X✝ : Type u_1
Y✝ : Type u_2
X : Type u_3
Y : Type u_4
A : Type u_5
inst✝ : TopologicalSpace X
c : A → X
f : A → Y
x : X
F : Filter Y
h : Tendsto f (comap c (𝓝 x)) F
V' : Set Y
V'_in : V' ∈ F
⊢ ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V'
Tactic:
sorry
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Tactic:
let y := f c
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Tactic:
have hy : Tendsto f (𝓝 c) (𝓝 y) := by
  rw [← (@nhdsWithin_eq_nhds _ _ c (closedBall c R)).mpr (closedBall_mem_nhds _ h0)]
  exact ContinuousOn.continuousWithinAt hf <| mem_closedBall_self (le_of_lt h0)
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Tactic:
rw [← sub_eq_zero, ← norm_le_zero_iff]
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ 0
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ 0
Tactic:
refine' le_of_forall_le_of_dense fun ε ε0 => _
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
obtain ⟨α, α0, hα⟩ := (nhds_basis_ball.tendsto_iff (nhds_basis_ball)).1 hy _
  (div_pos ε0 Real.two_pi_pos)
Proof state after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
set δ := α/2
Proof state after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Theorem: Cauchy_formula
Proof state before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have δ0 := half_pos α0
Proof state after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε