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

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
E' : Type u_5
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝¹² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹¹ : TopologicalSpace M'
inst✝¹⁰ : ChartedSpace H' M'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
s : Set (M × M')
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt[Prod.fst '' s] f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt[Prod.snd '' s] g p.2 dg
p₀ : E × E'
hp₀ : p₀ ∈ ↑((chartAt H p.1).symm.prod (chartAt H' p.2).symm) ∘ ↑(I.symm.prod I'.symm) ⁻¹' s
hp₁₁ : p₀.1 ∈ range ↑I
hp₁₂ : p₀.2 ∈ range ↑I'
⊢ p₀.2 ∈ ↑(chartAt H' p.2).symm ∘ ↑I'.symm ⁻¹' Prod.snd '' s

Tactic:
simp_all; grind

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ContMDiff I.tangent 𝓘(𝕜, E) n fun p ↦ p.snd

Tactic:
change CMDiff n ((id Prod.snd : ModelProd H E → E) ∘ (tangentBundleModelSpaceHomeomorph I))

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ContMDiff I.tangent 𝓘(𝕜, E) n (id Prod.snd ∘ ⇑(tangentBundleModelSpaceHomeomorph I))
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝²² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝²¹ : TopologicalSpace H
E : Type u_3
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹⁸ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁷ : NormedAddCommGroup E'
inst✝¹⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝¹⁵ : TopologicalSpace H''
E'' : Type u_7
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝¹² : TopologicalSpace G
inst✝¹¹ : ChartedSpace H G
M : Type u_9
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H' M
G' : Type u_11
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : ChartedSpace H'' G'
inst✝⁶ : Monoid G'
inst✝⁵ : SMul G G'
inst✝⁴ : MulAction G' M
inst✝³ : SMul G M
inst✝² : IsScalarTower G G' M
n : ℕ∞ω
inst✝¹ : ContMDiffSMul I I'' n G G'
inst✝ : ContMDiffSMul I'' I' n G' M
⊢ ContMDiff (I.prod I') I' n fun p ↦ (p.1 • 1) • p.2

Tactic:
exact (contMDiff_fst.smul contMDiff_const).smul (I := I'') contMDiff_snd

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

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
inst✝ : IsManifold I 1 M
x₀ x : M
hx : x ∈ (chartAt H x₀).source
this : MDiffAt (↑I ∘ ↑(chartAt H x₀)) x
⊢ Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x = mfderiv% ↑(extChartAt I x₀) x

Tactic:
simp [hx, mfderiv, this]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case inr
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : ι → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
⊢ ∃ i, x ∈ (find c ne i).toFun i

Tactic:
rcases mem_iUnion.1 ((v i).subset_iUnion hxs) with ⟨j, hj⟩

Goal state after:
case inr
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : ι → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
j : ι
hj : x ∈ (v i).toFun j
⊢ ∃ i, x ∈ (find c ne i).toFun i
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
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
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ x ∈ support ↑(fs.toFun (fs.ind x hx))

Tactic:
simp [fs.apply_ind x hx]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h.refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∀ (i : ι), IsClosed ((fun i ↦ closure (v i)) i)

Tactic:
· simp only [isClosed_closure, implies_true]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ f =ᵐ[μ.restrict t] g

Tactic:
rw [← sub_ae_eq_zero]
  have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
    exact sub_eq_zero.mpr (hfg_zero s hs hμs)
  have hfg_int : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn (f - g) s μ := fun s hs hμs =>
    (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
  exact ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hfg_int hfg' ht hμt

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 t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
rcases hs.exists_contMDiff_support_eq I with ⟨f, f_supp, f_diff, f_pos⟩
  rcases ht.isOpen_compl.exists_contMDiff_support_eq I with ⟨g, g_supp, g_diff, g_pos⟩
  have A : ∀ x, 0 < f x + g x := by
    intro x
    by_cases xs : x ∈ support f
    · have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
      linarith [g_pos x]
    · have : 0 < g x := by
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
      linarith [f_pos x]
  refine ⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩
  -- show that `f / (f + g)` is smooth
  · exact f_diff.div₀ (f_diff.add g_diff) (fun x ↦ ne_of_gt (A x))
  -- show that the range is included in `[0, 1]`
  · refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)
    apply div_le_one_of_le₀ _ (A x).le
    simpa only [le_add_iff_nonneg_right] using g_pos x
  -- show that the support is `s`
  · have B : support (fun x ↦ f x + g x) = univ := eq_univ_of_forall (fun x ↦ (A x).ne')
    simp only [support_div, f_supp, B, inter_univ]
  -- show that the function equals one exactly on `t`
  · intro x
    simp [div_eq_one_iff_eq (A x).ne', left_eq_add, ← notMem_support, g_supp]

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
⊢ ∃ G,
    (∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (Icc a b))) ∧
        liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)

Tactic:
have hfg : EqOn f g (Ioo a b) := fun x ⟨hxa, hxb⟩ => congrArg f <|
    min_eq_left hxb.le |>.symm ▸ (max_eq_right hxa.le).symm

Goal state after:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn f g (Ioo a b)
⊢ ∃ G,
    (∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (Icc a b))) ∧
        liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: ⊢ Tendsto (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) totalLengthFilter (𝓝 0)

Tactic:
by
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, (dist (E.2 i).1 (E.2 i).2)))
  · convert! ENNReal.tendsto_ofReal (Filter.tendsto_comap)
    simp
  · intro; simp
  · intro E
    simp only
    grw [measure_biUnion_finset_le]
    rw [ENNReal.ofReal_sum_of_nonneg (fun _ _ ↦ dist_nonneg)]
    apply Eq.le
    apply Finset.sum_congr rfl
    simp [uIoc, Real.dist_eq, max_sub_min_eq_abs']

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 δ
v : E
hv : v ∈ q
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 0, ‖f (x + x_1 • v) - f x - x_1 • L v‖ ≤ δ * ‖x_1‖

Tactic:
apply Asymptotics.IsLittleO.def ?_ δpos

Goal state after:
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 δ
v : E
hv : v ∈ q
⊢ (fun x_1 ↦ f (x + x_1 • v) - f x - x_1 • L v) =o[𝓝 0] fun x ↦ x
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
absolutelyContinuousOnInterval_iff

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:

Tactic:
_ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case inr
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab₀ : a ≤ b
hab : a < b
⊢ BoundedVariationOn f (Icc a b)

Tactic:
absolutelyContinuousOnInterval_iff

Goal state after:
case inr
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
⊢ BoundedVariationOn f (Icc a b)
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
by
  obtain ⟨s, s_count, s_dense⟩ : ∃ (s : Set E), s.Countable ∧ Dense s :=
    TopologicalSpace.exists_countable_dense E
  have hs : sphere 0 1 ⊆ closure s := by rw [s_dense.closure_eq]; exact subset_univ _
  filter_upwards [hf.ae_exists_fderiv_of_countable s_count]
  rintro x ⟨L, hL⟩
  exact (hf.hasFDerivAt_of_hasLineDerivAt_of_closure hs hL).differentiableAt

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

Goal state before:
pp: case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - √((1 - (1 - z).re) ^ 2 + (1 - z).im ^ 2))
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M

Tactic:
← h,

Goal state after:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)

Goal state after:
x : ℂ
h : cos x = 0
this : ¬DifferentiableAt ℂ tan x
⊢ deriv tan x = 1 / cos x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
⊢ HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x

Tactic:
have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
  simpa [cos_sq_arctan] using
    tanPartialHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)

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

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ cos y ^ 2 < 1 ^ 2 / √(y ^ 2 + 1) ^ 2

Tactic:
one_pow,

Goal state after:
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ cos y ^ 2 < 1 / √(y ^ 2 + 1) ^ 2
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: a x y : ℂ
⊢ angle (x / a) y = angle x (y * a)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
x y : ℂ
⊢ angle (x / 0) y = angle x (y * 0)

case inr
a x y : ℂ
ha : a ≠ 0
⊢ angle (x / a) y = angle x (y * a)
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle (x / y) 1) (angle (x / y) 1)
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
rwa [angle_div_left_eq_angle_mul_right, div_sub_one, norm_div, hy, div_one, one_mul]
      at this

Goal state after:
case inr
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this✝ : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
this : ‖x / y - 1‖ ∈ Icc (2 / π * angle x (1 * y)) (angle x (1 * y))
⊢ y ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x - y‖ = ‖x‖ + ‖y‖

Tactic:
by
  rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
    norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h]
  ring

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

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ ∅, MeromorphicOn (f i) U
h₂f : ∀ i ∈ ∅, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ divisor 1 U = 0

Tactic:
exact divisor_ofNat 1

Goal state after:
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
⊢ MeromorphicNFAt (fun a ↦ ∏ i ∈ s, f i a) x

Tactic:
convert! meromorphicNFAt_prod h₁f h₂f

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
x✝ : 𝕜
⊢ ∏ i ∈ s, f i x✝ = (∏ i ∈ s, f i) 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 : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
⊢ ENat.map (fun x ↦ ↑x) (analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose ⋯ • f z) x) - ↑(Exists.choose ⋯) = ↑n ↔
    ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
← h,

Goal state after:
case neg
𝕜 : 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 = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
⊢ ENat.map (fun x ↦ ↑x) ↑m - ↑(Exists.choose ⋯) = ↑n ↔
    ∃ 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 mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : toMeromorphicNFOn f U = f
⊢ MeromorphicNFOn f U

pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
⊢ toMeromorphicNFOn f U = f

Tactic:
· rw [h.symm]
    apply meromorphicNFOn_toMeromorphicNFOn

Goal state after:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h : MeromorphicNFOn f U
⊢ toMeromorphicNFOn f U = f
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2.refine_7
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a✝ : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a✝)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a✝ ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
N : Set A
haN : a✝ ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a✝} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a✝} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
a : A
⊢ (fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta) (0, a) = g (0, a)

Tactic:
rw [← g'_0]

Goal state after:
case refine_2.refine_7
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a✝ : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a✝)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a✝ ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
N : Set A
haN : a✝ ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a✝) = g (t', a✝)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a✝)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a✝} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a✝} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
a : A
⊢ (fun ta ↦ if ta.1 ≤ t n then g' ta else if f ta ∈ (q e).target then ↑(q e).symm (f ta) else g ta) (0, a) = g' (0, a)
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) x = ∏ᶠ (u : 𝕜), (x - u) ^ d u

Tactic:
meromorphicTrailingCoeffAt_factorizedRational h₁,

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ ∏ᶠ (u : 𝕜), (x - u) ^ update d x 0 u = ∏ᶠ (u : 𝕜), (x - u) ^ d u
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_5
F : ι → 𝕜 → 𝕜
h₁ : ∀ (c : ι), MeromorphicAt (F c) x
h₂ : ∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤
hF : ¬Function.HasFiniteMulSupport F
⊢ meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤

Tactic:
simp [finprod_of_not_hasFiniteMulSupport hF]

Goal state after: