Theorem: Barrier.potential_large (Ray/Dynamics/Potential.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
by_cases t0 : t = ∅
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : ¬t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : ¬t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
simp only [← ne_eq, ← Set.nonempty_iff_ne_empty] at t0
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
have pc : ContinuousOn (uncurry s.potential) t := by
  refine ContinuousOn.mono ?_ b.near
  intro ⟨c, z⟩ m; apply ContinuousAt.continuousWithinAt
  apply ContinuousAt.potential_of_reaches s; use 0; simpa only [Function.iterate_zero_apply]
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
rcases b.compact.exists_isMinOn t0 pc with ⟨⟨e, z⟩, ps, pm⟩
State after:
case neg.intro.mk.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z

State before:
case neg.intro.mk.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
use s.potential e z
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0 ∧ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0 ∧ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1
Tactic:
constructor
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0

case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∃ r > 0, ∀ (e : ℂ) (z : S), (e, z) ∈ t → r ≤ s.potential e z
Tactic:
use 1, zero_lt_one
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∀ (e : ℂ) (z : S), (e, z) ∈ t → 1 ≤ s.potential e z

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t = ∅
⊢ ∀ (e : ℂ) (z : S), (e, z) ∈ t → 1 ≤ s.potential e z
Tactic:
simp only [t0, gt_iff_lt, Set.mem_empty_iff_false, IsEmpty.forall_iff, forall_const,
  imp_true_iff, and_true_iff]
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ContinuousOn (uncurry s.potential) t
Tactic:
refine ContinuousOn.mono ?_ b.near
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ContinuousOn (uncurry s.potential) s.near

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
⊢ ContinuousOn (uncurry s.potential) s.near
Tactic:
intro ⟨c, z⟩ m
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousWithinAt (uncurry s.potential) s.near (c, z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousWithinAt (uncurry s.potential) s.near (c, z)
Tactic:
apply ContinuousAt.continuousWithinAt
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousAt (uncurry s.potential) (c, z)

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ContinuousAt (uncurry s.potential) (c, z)
Tactic:
apply ContinuousAt.potential_of_reaches s
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
use 0
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, (f c)^[0] z) ∈ s.near

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c✝ n t
t0 : t.Nonempty
c : ℂ
z : S
m : (c, z) ∈ s.near
⊢ (c, (f c)^[0] z) ∈ s.near
Tactic:
simpa only [Function.iterate_zero_apply]
State after:
no goals

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ s.potential e z > 0
Tactic:
have h := b.hole e
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : (e, a) ∉ t
⊢ s.potential e z > 0

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : (e, a) ∉ t
⊢ s.potential e z > 0
Tactic:
contrapose h
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : ¬s.potential e z > 0
⊢ ¬(e, a) ∉ t

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : ¬s.potential e z > 0
⊢ ¬(e, a) ∉ t
Tactic:
simp only [not_lt] at h
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
⊢ ¬(e, a) ∉ t

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
⊢ ¬(e, a) ∉ t
Tactic:
have h' := le_antisymm h s.potential_nonneg
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : s.potential e z = 0
⊢ ¬(e, a) ∉ t

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : s.potential e z = 0
⊢ ¬(e, a) ∉ t
Tactic:
simp only [s.potential_eq_zero, s.preimage_eq, exists_const] at h'
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : z = a
⊢ ¬(e, a) ∉ t

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
h : s.potential e z ≤ 0
h' : z = a
⊢ ¬(e, a) ∉ t
Tactic:
simp only [not_not, ← h', ps]
State after:
no goals

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e : ℂ
z : S
ps : (e, z) ∈ t
pm : IsMinOn (uncurry s.potential) t (e, z)
⊢ ∀ (e_1 : ℂ) (z_1 : S), (e_1, z_1) ∈ t → s.potential e z ≤ s.potential e_1 z_1
Tactic:
intro e z m
State after:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
pm : IsMinOn (uncurry s.potential) t (e✝, z✝)
e : ℂ
z : S
m : (e, z) ∈ t
⊢ s.potential e✝ z✝ ≤ s.potential e z

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
pm : IsMinOn (uncurry s.potential) t (e✝, z✝)
e : ℂ
z : S
m : (e, z) ∈ t
⊢ s.potential e✝ z✝ ≤ s.potential e z
Tactic:
simp only [isMinOn_iff, uncurry] at pm ⊢
State after:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
e : ℂ
z : S
m : (e, z) ∈ t
pm : ∀ x ∈ t, s.potential e✝ z✝ ≤ s.potential x.1 x.2
⊢ s.potential e✝ z✝ ≤ s.potential e z

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z✝¹ : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
e : ℂ
z : S
m : (e, z) ∈ t
pm : ∀ x ∈ t, s.potential e✝ z✝ ≤ s.potential x.1 x.2
⊢ s.potential e✝ z✝ ≤ s.potential e z
Tactic:
exact pm _ m
State after:
no goals