mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x✝ : ↑I
h✝ : ¬↑x✝ ≤ 1 / 2
⊢ p
      ({ toContinuousMap := cov.liftPath (↑γ') ((cov.liftPath (↑γ) e ⋯) 1) ⋯, source' := ⋯, target' := ⋯ }
        ⟨2 * ↑x✝ - 1, ⋯⟩) =
    γ' ⟨2 * ↑x✝ - 1, ⋯⟩

Tactic:
·

Goal state after:
case neg
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y z : X
e : E
hpe : x = p e
γ : Path x y
γ' : Path y z
x✝ : ↑I
h✝ : ¬↑x✝ ≤ 1 / 2
⊢ p
      ({ toContinuousMap := cov.liftPath (↑γ') ((cov.liftPath (↑γ) e ⋯) 1) ⋯, source' := ⋯, target' := ⋯ }
        ⟨2 * ↑x✝ - 1, ⋯⟩) =
    γ' ⟨2 * ↑x✝ - 1, ⋯⟩
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
⊢ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ ∈ 𝓝[≠] x

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
⊢ (U \ Subtype.val '' {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤})ᶜ ∈ 𝓝[≠] x
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ rexp 1 < 0.36787944116⁻¹

pp: ⊢ 0 < 0.36787944116

Tactic:
·

Goal state after:
⊢ rexp 1 < 0.36787944116⁻¹
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ rexp 1 < 0.36787944116⁻¹

Tactic:
refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_

Goal state after:
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 0 < 0.36787944116

Tactic:
·

Goal state after:
⊢ 0 < 0.36787944116
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h'₁a : f a ≠ 0
h' : AnalyticAt 𝕜 f a
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h'₁a : f a ≠ 0
h' : a ∈ Uᶜ
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h'₁a : f a ≠ 0
h' : AnalyticAt 𝕜 f a
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h'₁a : f a ≠ 0
h' : a ∈ Uᶜ
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ 0
a : 𝕜
h'₁a : f a ≠ 0
h' : a ∈ Uᶜ
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
⊢ H' = ⇑(cov.liftHomotopy H f H_0) →
    (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a

pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
x✝¹ : (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
H'_cont : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)
H'_lifts : p ∘ H' = ⇑H
H'_0 : ∀ (a : A), H' (0, a) = f a
x✝ : ↑I × A
t : ↑I
a : A
⊢ H' (t, a) = (cov.liftHomotopy H f H_0) (t, a)

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
⊢ H' = ⇑(cov.liftHomotopy H f H_0) →
    (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) ≠ ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x =
    meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤

pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x) ≠ 0

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
x✝¹ : (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
H'_cont : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)
H'_lifts : p ∘ H' = ⇑H
H'_0 : ∀ (a : A), H' (0, a) = f a
x✝ : ↑I × A
t : ↑I
a : A
⊢ H' (t, a) = (cov.liftHomotopy H f H_0) (t, a)

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
x✝¹ : (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
H'_cont : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)
H'_lifts : p ∘ H' = ⇑H
H'_0 : ∀ (a : A), H' (0, a) = f a
x✝ : ↑I × A
t : ↑I
a : A
⊢ H' (t, a) = (cov.liftHomotopy H f H_0) (t, a)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x) ≠ 0

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x) ≠ 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ (cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯) 0 = f₀' a

pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ ∀ (a_1 a' : ↑I),
    p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯)
          a_1) =
      p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯)
          a')

Tactic:
·

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ (cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯) 0 = f₀' a
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ ∀ (a_1 a' : ↑I),
    p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯)
          a_1) =
      p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯)
          a')

Tactic:
·

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
f₀ f₁ : C(A, X)
S : Set A
F : f₀.HomotopyRel f₁ S
inst✝ : PreconnectedSpace A
f₀' f₁' : C(A, E)
he : ∃ a ∈ S, f₀' a = f₁' a
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
t : ↑I
a : A
ha : a ∈ S
⊢ ∀ (a_1 a' : ↑I),
    p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯)
          a_1) =
      p
        ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const ↑I (t, a).2))) (f₀' (t, a).2) ⋯)
          a')
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : deriv g x ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : ¬MeromorphicAt f (g x)
⊢ meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : ¬MeromorphicAt f (x + c)
⊢ meromorphicOrderAt (f ∘ fun x ↦ x + c) x = meromorphicOrderAt f (x + c)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hg : AnalyticAt 𝕜 g x
hg' : g x ≠ 0
hf : ¬MeromorphicAt f x
⊢ meromorphicOrderAt (g • f) x = meromorphicOrderAt f x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ : C(↑I, A)
γ_0 : γ 0 = a₀
⊢ ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)

pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
⊢ Γ 1 = Γ' 1

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
γ : C(↑I, A)
γ_0 : γ 0 = a₀
⊢ ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a = z.im
⊢ ‖f z‖ ≤ C

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a < z.im
⊢ ‖f z‖ ≤ C

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a = z.im
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x

pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ^ (-divisor f (sphere 0 R)) x = (w - x) ^ (-divisor f (sphere 0 R)) x

Tactic:
·

Goal state after:
case e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h₃x : (divisor f (ball 0 R)) x = 0
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h₃x : ¬(divisor f (ball 0 R)) x = 0
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
x : ℂ
h₃x : (divisor f (ball 0 R)) x = 0
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ : C(↑I, A)
γ_0 : γ 0 = a₀
⊢ ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)

pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
⊢ Γ 1 = Γ' 1

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ : C(↑I, A)
γ_0 : γ 0 = a₀
⊢ ∃ Γ, Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)