internlm/Lean-Github huggingface dataset:
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 0.15 + (Complex.abs z).log.log < -0.15 + ((Complex.abs z).log.log + 0.548)
Tactic:
ring_nf
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 + (Complex.abs z).log.log < 199 / 500 + (Complex.abs z).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 + (Complex.abs z).log.log < 199 / 500 + (Complex.abs z).log.log
Tactic:
simp only [add_lt_add_iff_right]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 < 199 / 500
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 3 / 20 < 199 / 500
Tactic:
norm_num
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
⊢ 1 < Complex.abs c
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ 0 < (↑d)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ f d c ↑z = ↑w
Tactic:
rw [f, lift_coe', hw]
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ Complex.abs z ≤ Complex.abs w
Tactic:
rw [←hw]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ Complex.abs z ≤ Complex.abs (f' d c z)
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ Complex.abs z ≤ Complex.abs (f' d c z)
Tactic:
exact le_self_iter d (by linarith) cz 1
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ 3 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ 2 < Complex.abs c
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ 2 < Complex.abs w
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ Complex.abs c ≤ Complex.abs w
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ 3 ≤ Complex.abs w
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ 3 ≤ Complex.abs c
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
Tactic:
rw [←hw]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs (f' d c z)).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (Complex.abs z).log.log + 0.548 ≤ (Complex.abs (f' d c z)).log.log
Tactic:
exact log_log_iter (by linarith) cz
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ 4 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
⊢ ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
Tactic:
intro z z4 cz
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.15
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ 0.15
Tactic:
refine le_trans (iter_error_le_of_z4 d z4 cz) ?_
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.15
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.15
Tactic:
calc 0.8095 / (abs z * log (abs z))
  _ ≤ 0.8095 / (4 * log 4) := by bound
  _ ≤ 0.8095 / (4 * 1.386) := by bound [lt_log_4]
  _ ≤ 0.15 := by norm_num
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (Complex.abs z * (Complex.abs z).log) ≤ 0.8095 / (4 * log 4)
Tactic:
bound
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (4 * log 4) ≤ 0.8095 / (4 * 1.386)
Tactic:
bound [lt_log_4]
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c4 : 4 ≤ Complex.abs c
cz✝ : Complex.abs c ≤ Complex.abs z✝
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z✝).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z✝ = w
zw : Complex.abs z✝ ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z✝).log.log + 0.548 ≤ (Complex.abs w).log.log
z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0.8095 / (4 * 1.386) ≤ 0.15
Tactic:
norm_num
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
⊢ 4 ≤ Complex.abs w
Tactic:
linarith
Proof state after:
no goals
Theorem: eqn_near
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
Tactic:
have m : ∀ᶠ y : ℂ × ℂ in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near := by
  refine ContinuousAt.eventually_mem ?_ (s.isOpen_near.mem_nhds mem)
  exact continuousAt_fst.prod (s.continuousAt_iter continuousAt_fst holo.continuousAt)
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
Theorem: eqn_near
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
Tactic:
apply holo.eventually.mp
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Theorem: eqn_near
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x), HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
apply loc.mp
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n → HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Theorem: eqn_near
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n → HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
apply m.mp
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Theorem: eqn_near
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 : S
d n✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
apply eventually_of_forall
Proof state after:
case hp
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ (x : ℂ × ℂ),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Theorem: eqn_near
Proof state before:
case hp
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
⊢ ∀ (x : ℂ × ℂ),
    (x.1, (f x.1)^[n] (r x.1 x.2)) ∈ s.near →
      s.bottcherNear x.1 ((f x.1)^[n] (r x.1 x.2)) = x.2 ^ d ^ n →
        HolomorphicAt (I.prod I) I (uncurry r) x → Eqn s n r x
Tactic:
intro _ m l h
Proof state after:
case hp
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
x✝ : ℂ × ℂ
m : (x✝.1, (f x✝.1)^[n] (r x✝.1 x✝.2)) ∈ s.near
l : s.bottcherNear x✝.1 ((f x✝.1)^[n] (r x✝.1 x✝.2)) = x✝.2 ^ d ^ n
h : HolomorphicAt (I.prod I) I (uncurry r) x✝
⊢ Eqn s n r x✝
Theorem: eqn_near
Proof state before:
case hp
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
m✝ : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
x✝ : ℂ × ℂ
m : (x✝.1, (f x✝.1)^[n] (r x✝.1 x✝.2)) ∈ s.near
l : s.bottcherNear x✝.1 ((f x✝.1)^[n] (r x✝.1 x✝.2)) = x✝.2 ^ d ^ n
h : HolomorphicAt (I.prod I) I (uncurry r) x✝
⊢ Eqn s n r x✝
Tactic:
exact ⟨h, m, l⟩
Proof state after:
no goals