mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂
hf₁ : ¬MeromorphicAt f₁ x
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
have : ¬ MeromorphicAt f₂ x := by
      contrapose hf₁
      exact hf₁.congr hf₁₂.symm
    simp [hf₁, this]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
a✝ : ℕ
hn : analyticOrderAt f x = ↑a✝
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ↑a✝

Tactic:
[

Goal state after:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
a✝ : ℕ
hn : analyticOrderAt f x = ↑a✝
⊢ meromorphicOrderAt f x = ENat.map Nat.cast ↑a✝
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∑ i ∈ η₀.toFinset, divisor (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R) = -divisor f (ball 0 R)

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ ∑ i ∈ η₀.toFinset, divisor (canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R) = -divisor f (ball 0 R)
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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ g (x, a)
t✝ : ↑I
a✝ : A
N : Set A
haN : N ∈ 𝓝 a✝
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.univ ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x✝¹ : ↑I × A
t : ↑I
a : A
x✝ : (t, a) ∈ Set.univ ×ˢ N
left✝ : (t, a).1 ∈ Set.univ
ha : (t, a).2 ∈ N
⊢ g (t, a) = g' (t, a)

Tactic:
refine congr_fun (sep.eq_of_comp_eq homeo.isLocallyInjective (cont_A a)
    (cont_g'.comp_continuous (.prodMk_left a) fun _ ↦ ⟨⟨⟩, ha⟩) ?_ 0 (g'_0 a).symm) t

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
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
cont_A : ∀ (a : A), Continuous[_, inst✝²] fun x ↦ g (x, a)
t✝ : ↑I
a✝ : A
N : Set A
haN : N ∈ 𝓝 a✝
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.univ ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
x✝¹ : ↑I × A
t : ↑I
a : A
x✝ : (t, a) ∈ Set.univ ×ˢ N
left✝ : (t, a).1 ∈ Set.univ
ha : (t, a).2 ∈ N
⊢ (p ∘ fun x ↦ g (x, a)) = p ∘ g' ∘ fun x ↦ (x, a)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t✝ : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
t t' : ↑I
⊢ p ((Γ t) 1) = p ((Γ t') 1)

Tactic:
[

Goal state after:
case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t✝ : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
t t' : ↑I
⊢ p ((Γ t) 1) = p ((Γ t') 1)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ x) 0

Tactic:
[

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ x) 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case hg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := ⋯
g : 𝕜 → E := ⋯
⊢ AnalyticAt 𝕜 ((fun z ↦ (z - x) ^ (n₂ - n)) • g₂) x

Tactic:
apply (AnalyticAt.zpow_nonneg (by fun_prop) (sub_nonneg.2 (min_le_right n₁ n₂))).smul h₁g₂

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case refine_1
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ r * ↑g⁻¹ i i = 1

pp: case refine_2
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ ↑g⁻¹ i i * r = 1

Tactic:
· simpa [-mul_inv_cancel, ← hr, ← pow_succ',
      Nat.sub_one_add_one Fintype.card_pos.ne.symm] using
        Matrix.ext_iff.2 (Subtype.ext_iff.1 (mul_inv_cancel g)) i i

Goal state after:
case refine_2
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ ↑g⁻¹ i i * r = 1
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
hsq : ‖f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
[

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
hsq : ‖f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case «0»
a : Circle
j : Fin 2
⊢ ![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i ↦ ![(↑a).im, (↑a).re] j) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
fin_cases j

Goal state after:
case «0».«0»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨0, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨0, ⋯⟩))
      ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨1, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨1, ⋯⟩))
      ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case «1»
a : Circle
j : Fin 2
⊢ ![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i ↦ ![(↑a).im, (↑a).re] j) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
fin_cases j

Goal state after:
case «1».«0»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨0, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨0, ⋯⟩))
      ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«1»
a : Circle
⊢ ![(↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        (↑a).re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + (↑a).im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    Matrix.vecCons (![(↑a).re, -(↑a).im] ((fun i ↦ i) ⟨1, ⋯⟩)) (fun i ↦ ![(↑a).im, (↑a).re] ((fun i ↦ i) ⟨1, ⋯⟩))
      ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖map 1‖⁻¹ • (↑ℝ ↑map) x‖ = ‖x‖

Tactic:
this

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖map 1‖⁻¹ • (↑ℝ ↑map) (x • 1)‖ = ‖x‖
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
by
  rcases lt_trichotomy ‖x‖ R with h|h|h
  · -- The case where `x` is contained in `ball 0 R`. There, the divisor of `g` vanishes because `g`
    -- does not have zeros or poles. The divisor of `f` vanishes because `x` is not contained in the
    -- sphere.
    have : x ∉ sphere (0 : ℂ) R := by aesop
    have := (D.meromorphicNFOn (mem_closedBall_zero_iff.mpr h.le)).meromorphicOrderAt_eq_zero_iff.2
      (D.ne_zero x (by aesop))
    rw [divisor_apply D.meromorphicNFOn.meromorphicOn (mem_closedBall_zero_iff.mpr h.le)]
    simp_all
  · -- The case where `x` is contained in `sphere 0 R`. There, the orders of `f` and `g` agree
    -- because the canonical factors are analytic and do not vanish.
    have η₁ : AnalyticAt ℂ (∏ᶠ u, canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x := by
      refine analyticAt_finprod fun a ↦ ?_
      by_cases ha : a ∈ ball 0 R
      · exact (analyticOnNhd_canonicalFactor _ _ _ (by aesop)).zpow
          (canonicalFactor_ne_zero ha (by aesop) (by aesop))
      · simp_all only [mem_ball, dist_zero_right, not_lt,
          locallyFinsuppWithin.apply_eq_zero_of_notMem, neg_zero, zpow_zero]
        exact analyticAt_const
    have η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ u, canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g := by
      refine MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
        (U := closedBall 0 R) (D.meromorphicOn x (by aesop))
        (η₁.meromorphicAt.smul (D.meromorphicNFOn.meromorphicOn x (by aesop))) (by aesop) ?_
        D.eventuallyEq
      rw [← closure_ball 0 hR.ne']
      exact isOpen_ball.perfect_closure.2
    have : meromorphicOrderAt (∏ᶠ u, canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x = 0 := by
      refine η₁.meromorphicNFAt.meromorphicOrderAt_eq_zero_iff.2 (finprod_apply_ne_zero fun a ↦ ?_)
      by_cases ha : a ∈ ball 0 R
      · exact zpow_ne_zero _ (canonicalFactor_ne_zero ha (by aesop) (by aesop))
      · simp_all
    rw [divisor_apply (D.meromorphicOn.mono_set sphere_subset_closedBall) (by aesop),
      divisor_apply D.meromorphicNFOn.meromorphicOn (by aesop), meromorphicOrderAt_congr η₀,
      meromorphicOrderAt_smul η₁.meromorphicAt (D.meromorphicNFOn (by aesop)).meromorphicAt]
    simp_all
  · -- Trivial case: `x` is outside `closedBall 0 R`, so both divisors evaluate to zero.
    have : x ∉ sphere (0 : ℂ) R := by aesop
    simp_all

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := ⋯
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯
⊢ Set.MapsTo ((fun x_1 ↦ (x_1, (↑q (Γ (t n))).2)) ∘ γ.toFun) (Set.Icc 0 (t (n + 1)) ∩ closure {a | ¬a ≤ t n}) q.target

Tactic:
[

Goal state after:
case succ.refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := ⋯
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯
⊢ Set.MapsTo ((fun x_1 ↦ (x_1, (↑q (Γ (t n))).2)) ∘ γ.toFun) (Set.Icc 0 (t (n + 1)) ∩ closure {a | ¬a ≤ t n}) q.target
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
h₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
a : ℂ
h₁a : f a = ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) a
h₂a : g a = ((∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h) a
⊢ f a =
    (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
          ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
        h)
      a

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
h₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
a : ℂ
h₁a : f a = ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) a
h₂a : g a = ((∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h) a
⊢ f a =
    (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
          ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
        h)
      a
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
Γ : C(↑I, E)
⊢ Γ = cov.liftPath γ e γ_0 ↔ p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

Tactic:
[

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
Γ : C(↑I, E)
⊢ Γ = cov.liftPath γ e γ_0 ↔ p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e
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)
a : A
⊢ Continuous[_, inst✝²] fun x ↦ (cov.liftHomotopy H f H_0) (x, 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)
a : A
⊢ Continuous[_, inst✝²] fun x ↦ (cov.liftHomotopy H f H_0) (x, 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)
H' : C(↑I × A, E)
⊢ H' = cov.liftHomotopy H f H_0 ↔ p ∘ ⇑H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f 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)
H' : C(↑I × A, E)
⊢ H' = cov.liftHomotopy H f H_0 ↔ p ∘ ⇑H' = ⇑H ∧ ∀ (a : A), H' (0, a) = 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
t t' : ↑I
⊢ p ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) (f₀' a) ⋯) t) =
    p ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) (f₀' a) ⋯) t')

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
t t' : ↑I
⊢ p ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) (f₀' a) ⋯) t) =
    p ((cov.liftPath ((↑F).comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) (f₀' a) ⋯) t')
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)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), (cov.liftHomotopy (↑F) f₀' F_0).toFun (1, x) = f₁' x

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)
h₀ : p ∘ ⇑f₀' = ⇑f₀
h₁ : p ∘ ⇑f₁' = ⇑f₁
F_0 : ∀ (a : A), F (0, a) = p (f₀' a)
rel : ∀ (t : ↑I), ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a
a : A
ha : a ∈ S
he : f₀' a = f₁' a
⊢ ∀ (x : A), (cov.liftHomotopy (↑F) f₀' F_0).toFun (1, x) = f₁' x
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C(↑I, X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : γ₀ 0 = p e
h₁ : γ₁ 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
⊢ (cov.liftPath γ₀ e h₀) 0 = (cov.liftPath γ₁ e h₁) 0

Tactic:
[

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ₀ γ₁ : C(↑I, X)
h : γ₀.HomotopicRel γ₁ {0, 1}
e : E
h₀ : γ₀ 0 = p e
h₁ : γ₁ 0 = p e
H : γ₀.HomotopyRel γ₁ {0, 1}
⊢ (cov.liftPath γ₀ e h₀) 0 = (cov.liftPath γ₁ e h₁) 0
Module: Mathlib.Analysis.Meromorphic.Order

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

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt (f ∘ fun x ↦ x - c) x = meromorphicOrderAt f (x - c)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (Path.Homotopic.Quotient.mk γ₀).map { toFun := p, continuous_toFun := ⋯ } =
      (Path.Homotopic.Quotient.mk γ₁).map { toFun := p, continuous_toFun := ⋯ } →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁

Tactic:
[

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
e₀ e₁ : E
γ₀ γ₁ : Path e₀ e₁
⊢ (Path.Homotopic.Quotient.mk γ₀).map { toFun := p, continuous_toFun := ⋯ } =
      (Path.Homotopic.Quotient.mk γ₁).map { toFun := p, continuous_toFun := ⋯ } →
    Path.Homotopic.Quotient.mk γ₀ = Path.Homotopic.Quotient.mk γ₁