internlm/Lean-Github huggingface dataset:
Theorem: Bound.Real.rpow_le_rpow_of_exponent_le_or_ge
Proof state before:
case inl.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z
Tactic:
exact Real.rpow_le_rpow_of_exponent_le x1 yz
Proof state after:
no goals
Theorem: Bound.Real.rpow_le_rpow_of_exponent_le_or_ge
Proof state before:
case inr.intro.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z
Tactic:
exact Real.rpow_le_rpow_of_exponent_ge x0 x1 zy
Proof state after:
no goals
Theorem: swap_swap
Proof state before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
⊢ swap '' (swap '' s) = s
Tactic:
ext x
Proof state after:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ swap '' (swap '' s) ↔ x ∈ s
Theorem: swap_swap
Proof state before:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ swap '' (swap '' s) ↔ x ∈ s
Tactic:
simp only [Set.mem_image, Prod.exists]
Proof state after:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) ↔ x ∈ s
Theorem: swap_swap
Proof state before:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) ↔ x ∈ s
Tactic:
constructor
Proof state after:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) → x ∈ s

case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ s → ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x
Theorem: swap_swap
Proof state before:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) → x ∈ s
Tactic:
intro ⟨a,b,⟨⟨c,d,e,f⟩,g⟩⟩
Proof state after:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ x ∈ s
Theorem: swap_swap
Proof state before:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ x ∈ s
Tactic:
rw [←g, ←f]
Proof state after:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ (c, d).swap.swap ∈ s
Theorem: swap_swap
Proof state before:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ (c, d).swap.swap ∈ s
Tactic:
simpa only [swap]
Proof state after:
no goals
Theorem: swap_swap
Proof state before:
case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ s → ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x
Tactic:
intro m
Proof state after:
case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
m : x ∈ s
⊢ ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x
Theorem: swap_swap
Proof state before:
case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
m : x ∈ s
⊢ ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x
Tactic:
exact ⟨x.2,x.1,⟨x.1,x.2,m,rfl⟩,rfl⟩
Proof state after:
no goals
Theorem: isOpen_swap
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
s : Set (A × B)
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ IsOpen s → IsOpen (swap '' s)
Tactic:
rw [Set.image_swap_eq_preimage_swap]
Proof state after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
s : Set (A × B)
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ IsOpen s → IsOpen (swap ⁻¹' s)
Theorem: isOpen_swap
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
s : Set (A × B)
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ IsOpen s → IsOpen (swap ⁻¹' s)
Tactic:
exact IsOpen.preimage continuous_swap
Proof state after:
no goals
Theorem: swap_mem
Proof state before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (b, a) ∈ swap '' s ↔ (a, b) ∈ s
Tactic:
constructor
Proof state after:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (b, a) ∈ swap '' s → (a, b) ∈ s

case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (a, b) ∈ s → (b, a) ∈ swap '' s
Theorem: swap_mem
Proof state before:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (b, a) ∈ swap '' s → (a, b) ∈ s
Tactic:
intro m
Proof state after:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (b, a) ∈ swap '' s
⊢ (a, b) ∈ s
Theorem: swap_mem
Proof state before:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (b, a) ∈ swap '' s
⊢ (a, b) ∈ s
Tactic:
simp at m
Proof state after:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : ∃ a_1 b_1, (a_1, b_1) ∈ s ∧ b_1 = b ∧ a_1 = a
⊢ (a, b) ∈ s
Theorem: swap_mem
Proof state before:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : ∃ a_1 b_1, (a_1, b_1) ∈ s ∧ b_1 = b ∧ a_1 = a
⊢ (a, b) ∈ s
Tactic:
rcases m with ⟨a', b', m, hb, ha⟩
Proof state after:
case mp.intro.intro.intro.intro
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
a' : A
b' : B
m : (a', b') ∈ s
hb : b' = b
ha : a' = a
⊢ (a, b) ∈ s
Theorem: swap_mem
Proof state before:
case mp.intro.intro.intro.intro
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
a' : A
b' : B
m : (a', b') ∈ s
hb : b' = b
ha : a' = a
⊢ (a, b) ∈ s
Tactic:
rwa [← ha, ← hb]
Proof state after:
no goals
Theorem: swap_mem
Proof state before:
case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (a, b) ∈ s → (b, a) ∈ swap '' s
Tactic:
intro m
Proof state after:
case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (a, b) ∈ s
⊢ (b, a) ∈ swap '' s
Theorem: swap_mem
Proof state before:
case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (a, b) ∈ s
⊢ (b, a) ∈ swap '' s
Tactic:
exact Set.mem_image_of_mem swap m
Proof state after:
no goals
Theorem: swap_mem'
Proof state before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
⊢ x ∈ swap '' s ↔ x.swap ∈ s
Tactic:
have h := @swap_mem _ _ x.snd x.fst s
Proof state after:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (x.1, x.2) ∈ swap '' s ↔ (x.2, x.1) ∈ s
⊢ x ∈ swap '' s ↔ x.swap ∈ s
Theorem: swap_mem'
Proof state before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (x.1, x.2) ∈ swap '' s ↔ (x.2, x.1) ∈ s
⊢ x ∈ swap '' s ↔ x.swap ∈ s
Tactic:
simp at h ⊢
Proof state after:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ (x.2, x.1) ∈ s
⊢ (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ x.swap ∈ s
Theorem: swap_mem'
Proof state before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ (x.2, x.1) ∈ s
⊢ (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ x.swap ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: ball_prod_same'
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Tactic:
have s := ball_prod_same x.fst x.snd r
Proof state after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball (x.1, x.2) r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Theorem: ball_prod_same'
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball (x.1, x.2) r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Tactic:
simp only [Prod.mk.eta] at s
Proof state after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball x r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Theorem: ball_prod_same'
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
s : ball x.1 r ×ˢ ball x.2 r = ball x r
⊢ ball x r = ball x.1 r ×ˢ ball x.2 r
Tactic:
exact s.symm
Proof state after:
no goals
Theorem: ball_swap
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ball x.swap r = swap '' ball x r
Tactic:
apply Set.ext
Proof state after:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ∀ (x_1 : B × A), x_1 ∈ ball x.swap r ↔ x_1 ∈ swap '' ball x r
Theorem: ball_swap
Proof state before:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
⊢ ∀ (x_1 : B × A), x_1 ∈ ball x.swap r ↔ x_1 ∈ swap '' ball x r
Tactic:
intro y
Proof state after:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ y ∈ ball x.swap r ↔ y ∈ swap '' ball x r
Theorem: ball_swap
Proof state before:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ y ∈ ball x.swap r ↔ y ∈ swap '' ball x r
Tactic:
rw [swap_mem', Metric.mem_ball, Metric.mem_ball, Prod.dist_eq, Prod.dist_eq]
Proof state after:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ max (dist y.1 x.swap.1) (dist y.2 x.swap.2) < r ↔ max (dist y.swap.1 x.1) (dist y.swap.2 x.2) < r
Theorem: ball_swap
Proof state before:
case h
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x : A × B
r : ℝ
y : B × A
⊢ max (dist y.1 x.swap.1) (dist y.2 x.swap.2) < r ↔ max (dist y.swap.1 x.1) (dist y.swap.2 x.2) < r
Tactic:
simp only [ge_iff_le, max_lt_iff, Prod.fst_swap, Prod.snd_swap, and_comm]
Proof state after:
no goals
Theorem: dist_swap
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x y : A × B
⊢ dist x.swap y.swap = dist x y
Tactic:
rw [Prod.dist_eq, Prod.dist_eq]
Proof state after:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x y : A × B
⊢ max (dist x.swap.1 y.swap.1) (dist x.swap.2 y.swap.2) = max (dist x.1 y.1) (dist x.2 y.2)
Theorem: dist_swap
Proof state before:
A B C 𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : PseudoMetricSpace A
inst✝ : PseudoMetricSpace B
x y : A × B
⊢ max (dist x.swap.1 y.swap.1) (dist x.swap.2 y.swap.2) = max (dist x.1 y.1) (dist x.2 y.2)
Tactic:
simp only [Prod.fst_swap, Prod.snd_swap, ge_iff_le, max_comm]
Proof state after:
no goals
Theorem: Base.ball
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : ↑(closure s)
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball (↑x) r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball (↑x) r)).EventuallyEq g f
Tactic:
rcases x with ⟨x, m⟩
Proof state after:
case mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball (↑⟨x, m⟩) r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball (↑⟨x, m⟩) r)).EventuallyEq g f
Theorem: Base.ball
Proof state before:
case mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball (↑⟨x, m⟩) r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball (↑⟨x, m⟩) r)).EventuallyEq g f
Tactic:
simp only [Subtype.coe_mk]
Proof state after:
case mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Theorem: Base.ball
Proof state before:
case mk
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
rcases b.point m with ⟨g, pg, e⟩
Proof state after:
case mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg : ∀ᶠ (z : E) in 𝓝 x, p g z
e : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Theorem: Base.ball
Proof state before:
case mk.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg : ∀ᶠ (z : E) in 𝓝 x, p g z
e : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
rcases Metric.eventually_nhds_iff_ball.mp pg with ⟨r, rp, pg⟩
Proof state after:
case mk.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Theorem: Base.ball
Proof state before:
case mk.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
rcases Filter.frequently_iff.mp e (Metric.ball_mem_nhds _ rp) with ⟨y, yb, ys, e⟩
Proof state after:
case mk.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Theorem: Base.ball
Proof state before:
case mk.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
⊢ ∃ g r, 0 < r ∧ (∀ z ∈ Metric.ball x r, p g z) ∧ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
use g, r, rp, fun z zr ↦ pg z zr
Proof state after:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
⊢ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Theorem: Base.ball
Proof state before:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
⊢ (𝓝ˢ (s ∩ Metric.ball x r)).EventuallyEq g f
Tactic:
simp only [Filter.EventuallyEq, Filter.eventually_iff, mem_nhdsSet_iff_forall]
Proof state after:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
⊢ ∀ x_1 ∈ s ∩ Metric.ball x r, {x | g x = f x} ∈ 𝓝 x_1
Theorem: Base.ball
Proof state before:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
⊢ ∀ x_1 ∈ s ∩ Metric.ball x r, {x | g x = f x} ∈ 𝓝 x_1
Tactic:
intro z ⟨zs, zr⟩
Proof state after:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ {x | g x = f x} ∈ 𝓝 z
Theorem: Base.ball
Proof state before:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ {x | g x = f x} ∈ 𝓝 z
Tactic:
simp only [← Filter.eventually_iff]
Proof state after:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Theorem: Base.ball
Proof state before:
case right
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Tactic:
rcases local_preconnected_nhdsSet (b.convex.inter (convex_ball _ _)).isPreconnected n with
  ⟨u, uo, iu, up, uc⟩
Proof state after:
case right.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Theorem: Base.ball
Proof state before:
case right.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Tactic:
have eq := b.unique uo uc (fun _ m ↦ (up m).1) (fun _ m ↦ (up m).2) ⟨y, iu ⟨ys, yb⟩, e⟩
Proof state after:
case right.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
eq : EqOn g f u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Theorem: Base.ball
Proof state before:
case right.intro.intro.intro.intro
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
n : {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
u : Set E
uo : IsOpen u
iu : s ∩ Metric.ball x r ⊆ u
up : u ⊆ {z | p g z ∧ p f z}
uc : IsPreconnected u
eq : EqOn g f u
⊢ ∀ᶠ (x : E) in 𝓝 z, g x = f x
Tactic:
exact eq.eventuallyEq_of_mem (uo.mem_nhds (iu ⟨zs, zr⟩))
Proof state after:
no goals
Theorem: Base.ball
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ {z | p g z ∧ p f z} ∈ 𝓝ˢ (s ∩ Metric.ball x r)
Tactic:
refine Filter.inter_mem ?_ ?_
Proof state after:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ (fun z => p g z) ∈ 𝓝ˢ (s ∩ Metric.ball x r)

case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z✝ : E
b : Base p s f
x : E
m : x ∈ closure s
g : E → α
pg✝ : ∀ᶠ (z : E) in 𝓝 x, p g z
e✝ : ∃ᶠ (z : E) in 𝓝 x, z ∈ s ∧ g z = f z
r : ℝ
rp : r > 0
pg : ∀ y ∈ Metric.ball x r, p g y
y : E
yb : y ∈ Metric.ball x r
ys : y ∈ s
e : g y = f y
z : E
zs : z ∈ s
zr : z ∈ Metric.ball x r
⊢ (fun z => p f z) ∈ 𝓝ˢ (s ∩ Metric.ball x r)