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

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
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ (𝓝 c).HasBasis (fun x ↦ True) fun f ↦ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
← map_extChartAt_symm_nhdsWithin_range (I := I) c

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
c : M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ (map (↑(extChartAt I c).symm) (𝓝[range ↑I] ↑(extChartAt I c) c)).HasBasis (fun x ↦ True) fun f ↦
    ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ tsupport ⇑(ρ i)

Tactic:
apply subset_closure

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ support ⇑(ρ i)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: case refine_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := ⋯
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := ⋯
x : α
⊢ f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})

Tactic:
apply subset_closure

Goal state after:
case refine_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := ⋯
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := ⋯
x : α
⊢ f x ∈ Set.range f ∪ {0}
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
⊢ ‖a‖ / 2 < ‖↑x‖

Tactic:
have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this✝ : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
this : ‖a‖ ≤ ‖↑x‖ + ‖a - ↑x‖
⊢ ‖a‖ / 2 < ‖↑x‖
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: case hds
𝕜 : Type u_1
inst✝⁶ : Semiring 𝕜
ι✝ : Type u_2
E : ι✝ → Type u_3
inst✝⁵ : (i : ι✝) → AddCommGroup (E i)
inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)
inst✝³ : (i : ι✝) → TopologicalSpace (E i)
inst✝² : ∀ (i : ι✝), ContinuousAdd (E i)
inst✝¹ : ∀ (i : ι✝), ContinuousConstSMul 𝕜 (E i)
s : (i : ι✝) → Set (E i)
x : (i : ι✝) → E i
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
⊢ x + Pi.single i (d n) ∈ univ.pi fun i ↦ closure[inst✝³ i] (s i)

Tactic:
mem_univ_pi

Goal state after:
case hds
𝕜 : Type u_1
inst✝⁶ : Semiring 𝕜
ι✝ : Type u_2
E : ι✝ → Type u_3
inst✝⁵ : (i : ι✝) → AddCommGroup (E i)
inst✝⁴ : (i : ι✝) → Module 𝕜 (E i)
inst✝³ : (i : ι✝) → TopologicalSpace (E i)
inst✝² : ∀ (i : ι✝), ContinuousAdd (E i)
inst✝¹ : ∀ (i : ι✝), ContinuousConstSMul 𝕜 (E i)
s : (i : ι✝) → Set (E i)
x : (i : ι✝) → E i
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
⊢ ∀ (i_1 : ι✝), (x + Pi.single i (d n)) i_1 ∈ closure[inst✝³ i_1] (s i_1)
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ Tendsto (fun n ↦ (fun x ↦ c ^ x) n • d n) atTop (𝓝 0)

Tactic:
rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ ∀ (ib : ℕ), True → ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, (fun x ↦ c ^ x) x • d x ∈ Metric.ball 0 ((1 / 2) ^ ib)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
i : ℕ
hi : i ∈ Finset.range n
⊢ dist ((f • g) (I i).1) ((f • g) (I i).2) ≤
    dist (f (I i).1 • g (I i).1) (f (I i).1 • g (I i).2) + dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2)

Tactic:
exact dist_triangle _ _ _

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
⊢ ∃ y ∈ q, ‖w - y‖ < δ

Tactic:
simpa [← dist_eq_norm] using hq w_mem

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

Goal state before:

Tactic:
_ ≤ 1 * (1 - ‖z‖) := by gcongr
    _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
    _ ≤ _ := norm_sub_norm_le _ _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
s : Finset ↑u
z : ↑u
hz : z ∈ s
slope_bound : dist (slope f (↑z).1 (↑z).2) 0 ≤ r / (b - d)
⊢ g z ≤ r / (b - d) * ((↑z).2 - (↑z).1)

Tactic:
have : 0 < z.val.2 - z.val.1 := by linarith [hu₁ z (by simp)]

Goal state after:
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
s : Finset ↑u
z : ↑u
hz : z ∈ s
slope_bound : dist (slope f (↑z).1 (↑z).2) 0 ≤ r / (b - d)
this : 0 < (↑z).2 - (↑z).1
⊢ g z ≤ r / (b - d) * ((↑z).2 - (↑z).1)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.hv'.h
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x → iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1

Tactic:
filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a✝³ : ℝ
a✝² : a✝³ ≠ x₀
a✝¹ : a✝³ ≠ x
a✝ : a✝³ ∈ Ι x₀ x
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] a✝³ = deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) a✝³
Module: Mathlib.Topology.Order.ExtrClosure

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : Preorder Y
inst✝ : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst✝³] s)
⊢ IsLocalMaxOn f (closure[inst✝³] s) a

Tactic:
by
  rcases mem_nhdsWithin.1 h with ⟨U, Uo, aU, hU⟩
  refine mem_nhdsWithin.2 ⟨U, Uo, aU, ?_⟩
  rintro x ⟨hxU, hxs⟩
  refine ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU
  · rwa [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_inter_of_mem, ←
      mem_closure_iff_nhdsWithin_neBot]
    exact nhdsWithin_le_nhds (Uo.mem_nhds hxU)
  · exact (hc _ hxs).mono (inter_subset_right.trans subset_closure)

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

Goal state before:
pp: θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ (∃ n, 2 * I * θ = ↑π * I + ↑n * (2 * ↑π * I)) ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
refine exists_congr fun x => ?_

Goal state after:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ k, ↑k * ↑π = θ

Tactic:
simp only [tan, hθ, div_eq_zero_iff, sin_eq_zero_iff]

Goal state after:
θ : ℂ
hθ : cos θ ≠ 0
⊢ (∃ k, θ = ↑k * ↑π) ∨ False ↔ ∃ k, ↑k * ↑π = θ
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ MapsTo e (ball 0 1) (ball z r)

Tactic:
refine ((lipschitzWith_lineMap z w).mapsTo_ball (mt nndist_eq_zero.1 hne) 0 1).mono
      Subset.rfl ?_

Goal state after:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hr : dist 1 0 = 1
⊢ ball ((lineMap z w) 0) (↑(nndist z w) * 1) ⊆ ball z r
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b

Tactic:
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _

Goal state after:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ContinuousOn f (Icc w y)

x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ StrictMonoOn (deriv f) (Ioo w y)

x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∀ w_1 ∈ Ioo w y, deriv f w_1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (1 / cos x ^ 2) x

Tactic:
by
  convert! (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1
  rw_mod_cast [← sin_sq_add_cos_sq x]
  ring

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 < cos x

Tactic:
have := (sin_sq_lt_sq (by positivity)).trans_eq' (sin_sq_eq_half_sub (x / 2))
  ring_nf at this
  linarith

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * (π / 2)
ub : arctan x < π / 2
⊢ False

Tactic:
mul_lt_mul_iff_left₀ (by positivity)

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : arctan x < π / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * (π / 2) < 1 * (π / 2)
⊢ False

Tactic:
mul_lt_mul_iff_left₀ (by positivity)

Goal state after:
x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : 2 * ↑k + 1 < 1
⊢ False
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

Tactic:
suffices 0 ≤ slope f x y by
      simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add,
        not_le.mpr hxy, and_false, or_false] at this
      exact this.1

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ 0 ≤ slope f x y
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case ho
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := ⋯
g' : ℂ → ℂ := ⋯
⊢ (fun z ↦ g z - g c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹

Tactic:
refine Asymptotics.isBigO_refl (fun w ↦ ((w - c) ^ (n + 1))⁻¹) _ |>.mul_isLittleO hn
        |>.mono (nhdsWithin_le_nhds (s := {c}ᶜ)) |>.congr' ?_ ?_

Goal state after:
case ho.refine_1
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
⊢ (fun x ↦ ((x - c) ^ (n + 1))⁻¹ * (f x - f c)) =ᶠ[𝓝[≠] c] fun z ↦ g z - g c

case ho.refine_2
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun w ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : ℂ → ℂ := update g c ((𝓝[≠] c).limUnder g)
⊢ (fun x ↦ ((x - c) ^ (n + 1))⁻¹ * (x - c) ^ n) =ᶠ[𝓝[≠] c] fun z ↦ (z - c)⁻¹
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ normSq ↑z < 1

Tactic:
by
  rw [← Complex.norm_mul_self_eq_normSq, ← sq]
  exact z.sq_norm_lt_one

Goal state after:
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
⊢ normSq ↑z ≤ 1

Tactic:
by
  rw [← Complex.norm_mul_self_eq_normSq, ← sq]
  exact z.sq_norm_lt_one

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
⊢ a ∈ U → a ∈ (U \ {x | f₁ x = f₂ x})ᶜ → f₁ a = f₂ a

Tactic:
h₁a

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf₁ : MeromorphicOn f₁ U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f₁ x = f₂ x})ᶜ ∈ 𝓝[≠] x
this : U ∈ 𝓝[≠] x
a : 𝕜
h₁a : a ∈ U
⊢ a ∈ (U \ {x | f₁ x = f₂ x})ᶜ → f₁ a = f₂ a
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ divisor (∏ i ∈ s, f i) U = ∑ i ∈ s, divisor (f i) U

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
h₄f : ¬{σ ∈ s | f σ x = 0} = ∅
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x

Tactic:
rw [Finset.filter_eq_empty_iff] at h₄f

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
h₄f : ¬∀ ⦃x_1 : ι⦄, x_1 ∈ s → ¬f x_1 x = 0
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
μ : ι
hμ : μ ∈ s.erase τ
this : f μ x = 0
⊢ False

Tactic:
have : τ = μ := h₂f (by aesop) (by aesop)

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
h₃f : ∀ {τ : ι}, τ ∈ s → τ ∉ {σ ∈ s | f σ x = 0} → AnalyticAt 𝕜 (f τ) x
τ : ι
h₁τ : τ ∈ s
h₂τ : f τ x = 0
μ : ι
hμ : μ ∈ s.erase τ
this✝ : f μ x = 0
this : τ = μ
⊢ False
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
⊢ MeromorphicNFAt (f / g) x

Tactic:
div_eq_mul_inv

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
x : 𝕜
hf : AnalyticAt 𝕜 f x
hg : MeromorphicNFAt g x
hor : g x ≠ 0 ∨ f x ≠ 0
⊢ MeromorphicNFAt (f * g⁻¹) x
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
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
m : ℕ
p : 𝕜 → 𝕜
hq_ne : ¬q (g x) = 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hm : ↑m = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h₁p : AnalyticAt 𝕜 p x
h₂p : ¬p x = 0
h₃p : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ m * p z
a : 𝕜
⊢ g a - g x = (a - x) ^ m * p a →
    a ∈ g ⁻¹' {x_1 | f x_1 = ((fun x_2 ↦ x_2 - g x) ^ n • q) x_1} →
      (f ∘ g) a = ((fun x_1 ↦ x_1 - x) ^ (n * ↑m) • fun z ↦ p z ^ n • q (g z)) a

Tactic:
h₁a

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
m : ℕ
p : 𝕜 → 𝕜
hq_ne : ¬q (g x) = 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hm : ↑m = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h₁p : AnalyticAt 𝕜 p x
h₂p : ¬p x = 0
h₃p : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ m * p z
a : 𝕜
h₁a : g a - g x = (a - x) ^ m * p a
⊢ a ∈ g ⁻¹' {x_1 | f x_1 = ((fun x_2 ↦ x_2 - g x) ^ n • q) x_1} →
    (f ∘ g) a = ((fun x_1 ↦ x_1 - x) ^ (n * ↑m) • fun z ↦ p z ^ n • q (g z)) a
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h : 0 ≤ MeromorphicOn.divisor f U
x : 𝕜
⊢ x ∈ U → AnalyticAt 𝕜 f x

Tactic:
intro hx
    rw [← (h₁f hx).meromorphicOrderAt_nonneg_iff_analyticAt]
    have := h x
    simp only [Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, h₁f.meromorphicOn, hx,
      MeromorphicOn.divisor_apply, untop₀_nonneg] at this
    assumption

Goal state after:
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
U : Set 𝕜
hf : MeromorphicOn f U
this : U ∈ Filter.codiscreteWithin U
a : 𝕜
⊢ AnalyticAt 𝕜 f a → a ∈ U → f a = toMeromorphicNFOn f U a

Tactic:
h₁a

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
this : U ∈ Filter.codiscreteWithin U
a : 𝕜
h₁a : AnalyticAt 𝕜 f a
⊢ a ∈ U → f a = toMeromorphicNFOn f U a