mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) u x₀

Tactic:
by
  apply (ContMDiffWithinAt.sum_section_of_locallyFinite ht ht').congr' (t := Set.univ)
      (fun y hy ↦ ?_) (by grind) trivial
  rw [← tsum_eq_finsum (L := SummationFilter.unconditional ι)]
  choose U hu hfin using ht y
  have : {x | t x y ≠ 0} ⊆ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty} := by
    intro x hx
    rw [Set.mem_ofPred] at hx ⊢
    use y
    simpa using ⟨hx, mem_of_mem_nhds hu⟩
  exact Set.Finite.subset hfin this

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
i : M
⊢ ∃ g, support g = (chartAt H i).target ∩ ↑(chartAt H i).symm ⁻¹' s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) g ∧ range g ⊆ Icc 0 1

Tactic:
apply IsOpen.exists_contMDiff_support_eq_aux

Goal state after:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
i : M
⊢ IsOpen[inst✝⁶] ((chartAt H i).target ∩ ↑(chartAt H i).symm ⁻¹' s)
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∈ support ⇑(f c)
⊢ x ∈ tsupport ⇑(f c)

Tactic:
exact subset_tsupport _ Hx

Goal state after:
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : E → F
x y : E
t : 𝕜
hf : DifferentiableAt 𝕜 f (x + t • y)
⊢ deriv (fun s ↦ f (x + s • y)) t = (fderiv 𝕜 f (x + t • y)) y

Tactic:
have hg : Differentiable 𝕜 (fun (s : 𝕜) ↦ (x + s • y)) := by fun_prop
  convert fderiv_comp_deriv t hf hg.differentiableAt
  · simp
  · simpa using (deriv_smul_const (x := t) differentiableAt_id y).symm

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ (1 - b) • x + b • y ∈ ball 0 1

Tactic:
mem_ball_zero_iff,

Goal state after:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ ‖(1 - b) • x + b • y‖ < 1
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : (‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y ∈ ball 0 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
mem_ball_zero_iff,

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hg
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n ↦ z ^ n / (z - 1) + (0 + -1 / (z - 1))) atTop (𝓝 (0 + -1 / (z - 1)))

Tactic:
← zero_div (z - 1)

Goal state after:
case hg
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n ↦ z ^ n / (z - 1) + (0 / (z - 1) + -1 / (z - 1))) atTop (𝓝 (0 / (z - 1) + -1 / (z - 1)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
have := tan_add (x := x) (y := -y) <| by
    rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
    · refine .inl ⟨x_ne, fun l => ?_⟩
      rw [Ne, neg_eq_iff_eq_neg]
      convert! minus_y_ne (-l - 1) using 2
      push_cast
      ring
    · refine .inr ⟨x_eq, ?_⟩
      rcases minus_y_eq with ⟨l, rfl⟩
      use -l - 1
      push_cast
      ring

Goal state after:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
this : tan (x + -y) = (tan x + tan (-y)) / (1 - tan x * tan (-y))
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) = sin (a * (↑(x + 1) - 1 / 2) + b) - sin (a * (↑x - 1 / 2) + b)

Tactic:
rw [sin_sub_sin]

Goal state after:
case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) =
    2 * sin ((a * (↑(x + 1) - 1 / 2) + b - (a * (↑x - 1 / 2) + b)) / 2) *
      cos ((a * (↑(x + 1) - 1 / 2) + b + (a * (↑x - 1 / 2) + b)) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ |cos x| = 1 ↔ ∃ k, ↑k * π = x

Tactic:
by
  rw [← abs_one, abs_eq_abs, cos_eq_one_iff, cos_eq_neg_one_iff]
  constructor
  · rintro (⟨n, h⟩ | ⟨n, h⟩)
    · exact ⟨2 * n, by grind⟩
    · exact ⟨1 + n * 2, by grind⟩
  · rintro (⟨n, h⟩)
    obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
    · exact .inl ⟨n, by grind⟩
    · exact .inr ⟨n, by grind⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1

Tactic:
by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
simp only [arctan_neg, neg_add, neg_neg, ← sub_eq_add_neg _ π] at k

Goal state after:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case funProp.discharger
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ‖x.1‖ * ‖x.2‖ ≠ 0

Tactic:
simp [*]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h✝ : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : AccPt x (𝓟 U)
h : f =ᶠ[𝓝[≠] x] g
⊢ ∀ (a : 𝕜), deriv f a = deriv g a → a ∈ {x | deriv f x = deriv g x} ∪ Uᶜ

Tactic:
by simp +contextual

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
hacc : AccPt x (𝓟 U)
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
have h : f =ᶠ[𝓝[≠] x] g :=
      (hf x hx).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hg x hx) hx hacc h
    filter_upwards [h.nhdsNE_deriv] using by simp +contextual

Goal state after:
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
⊢ f z = (fun z ↦ f c + (z - c) • dslope f c z₀) z

Tactic:
have : dslope f c z = dslope f c z₀ := eq_of_norm_eq_of_norm_add_eq heq <| by
    simp only [heq, SameRay.rfl.norm_add, heq_add]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope (⇑e ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = ⇑e ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
this : dslope f c z = dslope f c z₀
⊢ f z = (fun z ↦ f c + (z - c) • dslope f c z₀) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
apply meromorphicOrderAt_congr

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : Set.EqOn f₁ f₂ Uᶜ
x : 𝕜
hx : x ∈ U
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt f₁ z = meromorphicOrderAt f₂ z

Tactic:
apply meromorphicOrderAt_congr

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
hU : Preperfect U
h : f₁ =ᶠ[codiscreteWithin U] f₂
z : 𝕜
hz : z ∈ U
⊢ f₁ =ᶠ[𝓝[≠] z] f₂
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x

Tactic:
apply meromorphicOrderAt_congr

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁ : f₁ =ᶠ[codiscreteWithin U] f₂
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
⊢ f₁ =ᶠ[𝓝[≠] x] f₂
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x < 0
h₃ : f x = 0
⊢ MeromorphicNFAt f x

Tactic:
right
      lift meromorphicOrderAt f x to ℤ using LT.lt.ne_top h₂ with n hn
      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff h₁).1 hn.symm
      use n, g, h₁g, h₂g
      filter_upwards [eventually_nhdsWithin_iff.1 h₃g]
      intro z hz
      by_cases h₁z : z = x
      · simp only [h₁z, Pi.smul_apply', Pi.pow_apply, sub_self]
        rw [h₃]
        apply (smul_eq_zero_of_left (zero_zpow n _) (g x)).symm
        by_contra hCon
        simp [hCon] at h₂
      · exact hz h₁z

Goal state after:
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 : 𝕜
hf : MeromorphicAt f x
h : analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0

Tactic:
rw [analyticOrderAt_eq_top] at h

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ ¬∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
rw [analyticOrderAt_eq_top] at h

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = 0
⊢ ¬∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U

Tactic:
· intro z hz
    rw [meromorphicNFAt_congr (toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds hf hz)]
    exact meromorphicNFAt_toMeromorphicNFAt

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : ¬MeromorphicOn f U
⊢ MeromorphicNFOn (toMeromorphicNFOn f U) U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ meromorphicOrderAt (toMeromorphicNFOn f U) x = meromorphicOrderAt f x

Tactic:
apply meromorphicOrderAt_congr

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
⊢ toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
x : 𝕜
h : ∀ σ ∈ s, MeromorphicAt (f σ) x
⊢ meromorphicTrailingCoeffAt (fun z ↦ ∏ n ∈ s, f n z) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x

Tactic:
convert! meromorphicTrailingCoeffAt_prod h
  simp

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

Goal state before:
pp: case neg.e_a
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝¹ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this✝ : u₀ ∈ Finite.toFinset hd
this : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ update d u₀ 0 u) ⊆ ↑((Finite.toFinset hd).erase u₀)
⊢ ∏ x ∈ (Finite.toFinset hd).erase u₀, (fun x_1 ↦ x_1 - x) ^ d x = ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d u₀ 0 u

Tactic:
simp_all [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]

Goal state after:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ ball 0 R
⊢ canonicalFactor R w z = 0 ↔ z = w

Tactic:
constructor
  · contrapose
    exact canonicalFactor_ne_zero hw (ball_subset_closedBall hz)
  · simp_all

Goal state after:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
⊢ 0 < R ∧ z - w ≠ 0

Tactic:
grind [mem_ball_zero_iff, norm_nonneg, mem_sphere_zero_iff_norm]

Goal state after:
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ?m.73

Tactic:
by simpa [mem_sphere_zero_iff_norm] using hz

Goal state after:
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
⊢ divisor (∏ᶠ (u : ℂ), canonicalFactor R u ^ (divisor f (ball 0 R)) u) (ball 0 R) = -divisor f (ball 0 R)

Tactic:
finprod_eq_prod_of_mulSupport_subset_of_finite _ (by aesop) η₀,

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
⊢ divisor (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (divisor f (ball 0 R)) i) (ball 0 R) = -divisor f (ball 0 R)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0

Tactic:
rw [← I_re]
      exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I

Goal state after:
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
U : X → Set X := fun x ↦ ⋯.choose
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
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 1)
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 1)
Γ_0 : Γ 0 = e
⊢ ContinuousOn Γ Set.univ

Tactic:
by convert! cont; rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩

Goal state after:
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
x✝ : DifferentiableWithinAt ℝ f s x ∧ (fderivWithin ℝ f s x) I = I • (fderivWithin ℝ f s x) 1
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x) I = I • (fderivWithin ℝ f s x) 1
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
apply (differentiableWithinAt_iff_restrictScalars ℝ h₁ hs).2
    use (fderivWithin ℝ f s x).complexOfReal h₂
    rfl

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

Goal state before:
pp: 𝕜 : 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 : AnalyticAt 𝕜 f a ∨ a ∈ Uᶜ
h'₁a : f a ≠ 0
⊢ a ∈ U → ∃ (_ : a ∈ U), ¬meromorphicOrderAt f a = 0 → meromorphicOrderAt f a = ⊤

Tactic:
rcases h₁a with h' | h'

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 = ⊤

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: 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
⊢ (H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) 0 = p (f a)

Tactic:
simp [*]

Goal state after: