internlm/Lean-Github huggingface dataset:
Theorem: Nat.ge_mod
Proof state before:
case a
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ n✝ < succ x
Tactic:
apply Nat.lt_of_succ_le
Proof state after:
case a.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ succ x
Theorem: Nat.ge_mod
Proof state before:
case a.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ succ x
Tactic:
apply Nat.le_succ_of_le
Proof state after:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ x
Theorem: Nat.ge_mod
Proof state before:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ x
Tactic:
rw [←hm]
Proof state after:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ x - n ≤ x
Theorem: Nat.ge_mod
Proof state before:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ x - n ≤ x
Tactic:
apply sub_le
Proof state after:
no goals
Theorem: Nat.ge_mod
Proof state before:
case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ succ (succ x) < succ n + 1
Tactic:
apply Nat.succ_lt_succ_iff.mpr
Proof state after:
case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ x + 1 < n + 1
Theorem: Nat.ge_mod
Proof state before:
case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ x + 1 < n + 1
Tactic:
apply not_le.mp h
Proof state after:
no goals
Theorem: not_le_mod
Proof state before:
x n : ℕ
⊢ ¬n + 1 ≤ x % (n + 1)
Tactic:
simp only [not_le, Nat.ge_mod]
Proof state after:
no goals
Theorem: sumOfSequence_eq
Proof state before:
n : ℕ
⊢ sumOfSequence n = n * (n + 1) / 2
Tactic:
simp [Nat.mul_add]
Proof state after:
n : ℕ
⊢ sumOfSequence n = (n * n + n) / 2
Theorem: sumOfSequence_eq
Proof state before:
n : ℕ
⊢ sumOfSequence n = (n * n + n) / 2
Tactic:
induction n
Proof state after:
case zero

⊢ sumOfSequence Nat.zero = (Nat.zero * Nat.zero + Nat.zero) / 2

case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2
Theorem: sumOfSequence_eq
Proof state before:
case zero

⊢ sumOfSequence Nat.zero = (Nat.zero * Nat.zero + Nat.zero) / 2

case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2
Tactic:
next      => rfl
Proof state after:
case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2
Theorem: sumOfSequence_eq
Proof state before:
case succ
n✝ : ℕ
n_ih✝ : sumOfSequence n✝ = (n✝ * n✝ + n✝) / 2
⊢ sumOfSequence (Nat.succ n✝) = (Nat.succ n✝ * Nat.succ n✝ + Nat.succ n✝) / 2
Tactic:
next n ih =>
  simp only [sumOfSequence, ih, Nat.add_succ, add_zero, Nat.succ_mul, Nat.mul_succ, Nat.succ_add]
  simp [
    Nat.add_div (b:=2),
    Nat.add_assoc (_+n) n n,
    ←Nat.mul_two n,
    Nat.add_div (b := n*2)
  ]
Proof state after:
no goals
Theorem: sumOfSequence_eq
Proof state before:
⊢ sumOfSequence Nat.zero = (Nat.zero * Nat.zero + Nat.zero) / 2
Tactic:
rfl
Proof state after:
no goals
Theorem: sumOfSequence_eq
Proof state before:
n : ℕ
ih : sumOfSequence n = (n * n + n) / 2
⊢ sumOfSequence (Nat.succ n) = (Nat.succ n * Nat.succ n + Nat.succ n) / 2
Tactic:
simp only [sumOfSequence, ih, Nat.add_succ, add_zero, Nat.succ_mul, Nat.mul_succ, Nat.succ_add]
Proof state after:
n : ℕ
ih : sumOfSequence n = (n * n + n) / 2
⊢ Nat.succ ((n * n + n) / 2 + n) = Nat.succ (Nat.succ (n * n + n + n + n)) / 2
Theorem: sumOfSequence_eq
Proof state before:
n : ℕ
ih : sumOfSequence n = (n * n + n) / 2
⊢ Nat.succ ((n * n + n) / 2 + n) = Nat.succ (Nat.succ (n * n + n + n + n)) / 2
Tactic:
simp [
  Nat.add_div (b:=2),
  Nat.add_assoc (_+n) n n,
  ←Nat.mul_two n,
  Nat.add_div (b := n*2)
]
Proof state after:
no goals
Theorem: sumOfSequence_eq
Proof state before:
n : ℕ
⊢ sumOfSequence n = n * (n + 1) / 2
Tactic:
sorry
Proof state after:
no goals
Theorem: LeanDemo.zero_eq
Proof state before:
⊢ 0 = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.one_eq_succ_zero
Proof state before:
⊢ 1 = succ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.two_eq_succ_one
Proof state before:
⊢ 2 = succ 1
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.three_eq_succ_two
Proof state before:
⊢ 3 = succ 2
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.three_eq_succ_succ_succ_zero
Proof state before:
⊢ 3 = succ (succ (succ zero))
Tactic:
rw [three_eq_succ_two]
Proof state after:
⊢ succ 2 = succ (succ (succ zero))
Theorem: LeanDemo.three_eq_succ_succ_succ_zero
Proof state before:
⊢ succ 2 = succ (succ (succ zero))
Tactic:
rw [two_eq_succ_one]
Proof state after:
⊢ succ (succ 1) = succ (succ (succ zero))
Theorem: LeanDemo.three_eq_succ_succ_succ_zero
Proof state before:
⊢ succ (succ 1) = succ (succ (succ zero))
Tactic:
rw [one_eq_succ_zero]
Proof state after:
⊢ succ (succ (succ 0)) = succ (succ (succ zero))
Theorem: LeanDemo.three_eq_succ_succ_succ_zero
Proof state before:
⊢ succ (succ (succ 0)) = succ (succ (succ zero))
Tactic:
rw [zero_eq]
Proof state after:
no goals
Theorem: LeanDemo.three_eq_succ_succ_succ_zero'
Proof state before:
⊢ 3 = succ (succ (succ zero))
Tactic:
rw [three_eq_succ_two, two_eq_succ_one, one_eq_succ_zero, zero_eq]
Proof state after:
no goals
Theorem: LeanDemo.add_zero
Proof state before:
⊢ ∀ (x : Nat), x + 0 = x
Tactic:
intro y
Proof state after:
y : Nat
⊢ y + 0 = y
Theorem: LeanDemo.add_zero
Proof state before:
y : Nat
⊢ y + 0 = y
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.add_succ
Proof state before:
⊢ ∀ (x y : Nat), x + succ y = succ (x + y)
Tactic:
intro x y
Proof state after:
x y : Nat
⊢ x + succ y = succ (x + y)
Theorem: LeanDemo.add_succ
Proof state before:
x y : Nat
⊢ x + succ y = succ (x + y)
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.zero_add
Proof state before:
⊢ ∀ (x : Nat), 0 + x = x
Tactic:
intro x
Proof state after:
x : Nat
⊢ 0 + x = x
Theorem: LeanDemo.zero_add
Proof state before:
x : Nat
⊢ 0 + x = x
Tactic:
induction x
Proof state after:
case zero

⊢ 0 + zero = zero

case succ
n✝ : Nat
n_ih✝ : 0 + n✝ = n✝
⊢ 0 + succ n✝ = succ n✝
Theorem: LeanDemo.zero_add
Proof state before:
⊢ 0 + zero = zero
Tactic:
case zero         => 
  rfl
Proof state after:
no goals
Theorem: LeanDemo.zero_add
Proof state before:
x' : Nat
ih : 0 + x' = x'
⊢ 0 + succ x' = succ x'
Tactic:
case succ x' ih   =>
  rw [add_succ, ih]
Proof state after:
no goals
Theorem: LeanDemo.zero_add
Proof state before:
⊢ 0 + zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.zero_add
Proof state before:
x' : Nat
ih : 0 + x' = x'
⊢ 0 + succ x' = succ x'
Tactic:
rw [add_succ, ih]
Proof state after:
no goals
Theorem: LeanDemo.succ_add
Proof state before:
x y : Nat
⊢ succ x + y = succ (x + y)
Tactic:
induction y
Proof state after:
case zero
x : Nat
⊢ succ x + zero = succ (x + zero)

case succ
x n✝ : Nat
n_ih✝ : succ x + n✝ = succ (x + n✝)
⊢ succ x + succ n✝ = succ (x + succ n✝)
Theorem: LeanDemo.succ_add
Proof state before:
x : Nat
⊢ succ x + zero = succ (x + zero)
Tactic:
case zero =>      rfl
Proof state after:
no goals
Theorem: LeanDemo.succ_add
Proof state before:
x y : Nat
ih : succ x + y = succ (x + y)
⊢ succ x + succ y = succ (x + succ y)
Tactic:
case succ y ih => rw [add_succ, add_succ, ih]
Proof state after:
no goals
Theorem: LeanDemo.succ_add
Proof state before:
x : Nat
⊢ succ x + zero = succ (x + zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanDemo.succ_add
Proof state before:
x y : Nat
ih : succ x + y = succ (x + y)
⊢ succ x + succ y = succ (x + succ y)
Tactic:
rw [add_succ, add_succ, ih]
Proof state after:
no goals
Theorem: LeanDemo.add_comm
Proof state before:
x y : Nat
⊢ x + y = y + x
Tactic:
induction y
Proof state after:
case zero
x : Nat
⊢ x + zero = zero + x

case succ
x n✝ : Nat
n_ih✝ : x + n✝ = n✝ + x
⊢ x + succ n✝ = succ n✝ + x
Theorem: LeanDemo.add_comm
Proof state before:
x : Nat
⊢ x + zero = zero + x
Tactic:
case zero =>
  rw [←zero_eq, zero_add, add_zero]
Proof state after:
no goals
Theorem: LeanDemo.add_comm
Proof state before:
x y : Nat
ih : x + y = y + x
⊢ x + succ y = succ y + x
Tactic:
case succ y ih =>
  sorry
Proof state after:
no goals
Theorem: LeanDemo.add_comm
Proof state before:
x : Nat
⊢ x + zero = zero + x
Tactic:
rw [←zero_eq, zero_add, add_zero]
Proof state after:
no goals
Theorem: LeanDemo.add_comm
Proof state before:
x y : Nat
ih : x + y = y + x
⊢ x + succ y = succ y + x
Tactic:
sorry
Proof state after:
no goals
Theorem: LeanDemo.add_assoc
Proof state before:
x y z : Nat
⊢ x + y + z = x + (y + z)
Tactic:
sorry
Proof state after:
no goals
Theorem: Super.nonempty_ps
Proof 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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
⊢ 1 ∈ s.ps c
Tactic:
simp only [Super.ps, mem_setOf, eq_self_iff_true, true_or_iff]
Proof state after:
no goals
Theorem: Super.compact_ps
Proof 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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
⊢ IsCompact (s.ps c)
Tactic:
have pc : Continuous (s.potential c) := (Continuous.potential s).along_snd
Proof 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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
⊢ IsCompact (s.ps c)
Theorem: Super.compact_ps
Proof 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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
⊢ IsCompact (s.ps c)
Tactic:
have c1 : IsCompact {(1 : ℝ)} := isCompact_singleton
Proof 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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ IsCompact (s.ps c)
Theorem: Super.compact_ps
Proof 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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ IsCompact (s.ps c)
Tactic:
convert c1.union ((s.isClosed_critical_not_a.snd_preimage c).isCompact.image pc)
Proof state after:
case h.e'_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ s.ps c = {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Theorem: Super.compact_ps
Proof state before:
case h.e'_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ s.ps c = {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Tactic:
apply Set.ext
Proof state after:
case h.e'_3.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ ∀ (x : ℝ), x ∈ s.ps c ↔ x ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ ∀ (x : ℝ), x ∈ s.ps c ↔ x ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Tactic:
intro p
Proof state after:
case h.e'_3.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ p ∈ s.ps c ↔ p ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ p ∈ s.ps c ↔ p ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Tactic:
simp only [mem_setOf, Super.ps, mem_singleton_iff, mem_union, mem_image, Ne, ←
  s.potential_eq_zero_of_onePreimage c]
Proof state after:
case h.e'_3.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    p = 1 ∨ ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    p = 1 ∨ ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p
Tactic:
apply or_congr_right
Proof state after:
case h.e'_3.h.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p
Tactic:
constructor
Proof state after:
case h.e'_3.h.h.mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) →
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p

case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.h.mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) →
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p

case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
intro ⟨p0, z, e, c⟩
Proof state after:
case h.e'_3.h.h.mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
p0 : ¬p = 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.h.mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
p0 : ¬p = 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
rw [← e] at p0
Proof state after:
case h.e'_3.h.h.mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.h.mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
exact ⟨z, ⟨c, p0⟩, e⟩
Proof state after:
case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
intro ⟨z, ⟨c, p0⟩, e⟩
Proof state after:
case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z
Tactic:
rw [e] at p0
Proof state after:
case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬p = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z
Theorem: Super.compact_ps
Proof state before:
case h.e'_3.h.h.mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬p = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z
Tactic:
exact ⟨p0, z, e, c⟩
Proof state after:
no goals