Theorem: critical_f (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ Critical (f d c) z ↔ z = 0 ∨ z = ∞
Tactic:
induction' z using OnePoint.rec with z
State after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Critical (f d c) ∞ ↔ ∞ = 0 ∨ ∞ = ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞

State before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Critical (f d c) ∞ ↔ ∞ = 0 ∨ ∞ = ∞
Tactic:
simp only [(superF d).critical_a, or_true]
State after:
no goals

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞
Tactic:
have zx : ∀ x : ℂ, (0 : ℂ →L[ℂ] ℂ) x = 0 := fun x ↦ ContinuousLinearMap.zero_apply _
State after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ Critical (f d c) ↑z ↔ ↑z = 0 ∨ ↑z = ∞
Tactic:
simp only [Critical, mfderiv, (holomorphicF (c, z)).along_snd.mdifferentiableAt, if_pos,
  ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ, writtenInExtChartAt_coe_f,
  RiemannSphere.extChartAt_coe, coePartialEquiv_symm_apply, toComplex_coe, coe_eq_zero,
  coe_eq_inf_iff, or_false_iff, ← deriv_fderiv, deriv_f', ContinuousLinearMap.ext_iff,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, Algebra.id.smul_eq_mul,
  one_mul, mul_eq_zero, Nat.cast_eq_zero, d_ne_zero, false_or_iff,
  pow_eq_zero_iff (d_minus_one_pos d).ne', zx]
State after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) ↔ z = 0

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) ↔ z = 0
Tactic:
constructor
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) → z = 0

case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ z = 0 → ∀ (x : ℂ), x = 0 ∨ z = 0

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ (∀ (x : ℂ), x = 0 ∨ z = 0) → z = 0
Tactic:
intro h
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : ∀ (x : ℂ), x = 0 ∨ z = 0
⊢ z = 0

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : ∀ (x : ℂ), x = 0 ∨ z = 0
⊢ z = 0
Tactic:
specialize h 1
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : 1 = 0 ∨ z = 0
⊢ z = 0

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : 1 = 0 ∨ z = 0
⊢ z = 0
Tactic:
simp only [one_mul, mul_eq_zero, one_ne_zero, false_or_iff] at h
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : z = 0
⊢ z = 0

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
h : z = 0
⊢ z = 0
Tactic:
exact h
State after:
no goals

State before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
zx : ∀ (x : ℂ), 0 x = 0
⊢ z = 0 → ∀ (x : ℂ), x = 0 ∨ z = 0
Tactic:
exact fun h x ↦ Or.inr h
State after:
no goals