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

Goal state before:
pp: case h
𝕜 : 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 : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffAt[(extChartAt I x).source] (↑(extChartAt I x).symm y)
this :
  mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    mfderiv[(extChartAt I x).source] ↑(extChartAt I x) (↑(extChartAt I x).symm y)
z : M
hz : z ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x) z ∈ (extChartAt I x).target

Tactic:
exact PartialEquiv.map_source (extChartAt I x) hz

Goal state after:
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 • p.2

Tactic:
suffices CMDiff n (fun p : G × M ↦ (p.1 • (1 : G')) • p.2) by simpa
    exact (contMDiff_fst.smul contMDiff_const).smul (I := I'') contMDiff_snd

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : 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
i : ι
hi : i ∈ chainSupCarrier c
v : PartialRefinement u s p
hv : v ∈ c ∧ i ∈ v.carrier
⊢ p ((find c ne i).toFun i)

Tactic:
rw [find_apply_of_mem hc ne hv.1 hv.2]

Goal state after:
ι : 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
i : ι
hi : i ∈ chainSupCarrier c
v : PartialRefinement u s p
hv : v ∈ c ∧ i ∈ v.carrier
⊢ p (v.toFun i)
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 ↦ (ρ x_1) x) ⊆ ↑I
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 ↦ (ρ x_1) x) ⊆ ↑I

Tactic:
use I

Goal state after:
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 ↦ (ρ x_1) x) ⊆ ↑I
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 ↦ (ρ x_1) x) ⊆ ↑I
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
⊢ (support fun i ↦ f.toPOUFun i x) ⊆ ↑s

Tactic:
rw [hs]

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
⊢ (support fun i ↦ f.toPOUFun i x) ⊆ {i | (f i) x ≠ 0}
Module: Mathlib.Topology.MetricSpace.PartitionOfUnity

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i

Tactic:
suffices ∀ i, x ∈ K i → ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i by
    apply mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
      (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
    apply univ_mem'
    rintro ⟨r, y⟩ hxy hyU i hi
    simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
    exact hyU _ (hxy _ hi)

Goal state after:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i
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 g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
⊢ Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ (C * ‖v‖) * ‖g x‖)
  · filter_upwards with t
    apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
    apply aestronglyMeasurable_const.fun_smul
    apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
    apply AEMeasurable.aestronglyMeasurable
    exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)
  · filter_upwards [self_mem_nhdsWithin] with t (ht : 0 < t)
    filter_upwards with x
    calc ‖t⁻¹ • (f (x + t • v) - f x) * g x‖
      = (t⁻¹ * ‖f (x + t • v) - f x‖) * ‖g x‖ := by simp [norm_mul, ht.le]
    _ ≤ (t⁻¹ * (C * ‖(x + t • v) - x‖)) * ‖g x‖ := by
      gcongr; exact LipschitzWith.norm_sub_le hf (x + t • v) x
    _ = (C * ‖v‖) * ‖g x‖ := by simp [field, norm_smul, abs_of_nonneg ht.le]
  · exact hg.norm.const_mul _
  · filter_upwards [hf.ae_lineDifferentiableAt v] with x hx
    exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ∞ → ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 0

Tactic:
intro s hs hμs
    rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
    rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs,
      trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs
    rw [← integral_trim hm hf_meas_m]
    exact hf_zero _ (hs.inter ht_meas) hμs

Goal state after:
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)

Tactic:
rcases le_total n m with hnm | hmn
  · rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
  · refine Succ.rec ?_ ?_ hmn
    · simp
    · intro k hmk ihk
      rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
      by_cases hk : IsMax k
      · rw [hk.succ_eq, Ioc_self, empty_union]
      · rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]

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

Goal state before:
pp: case hgf
⊢ (fun x ↦ 0) ≤ fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

pp: case hfh
⊢ (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)

Tactic:
· intro; simp

Goal state after:
case hfh
⊢ (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hgf
a b : ℝ
⊢ (fun x ↦ 0) ≤ fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

pp: case hfh
a b : ℝ
⊢ (fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

Tactic:
· intro; simp

Goal state after:
case hfh
a b : ℝ
⊢ (fun E ↦ (volume.restrict (uIoc a b)) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
⊢ dist (f d) (f b) ≤ y

Tactic:
have hT₄ (s : Finset u) := (u_coe s).intervalGapsWithin_pairwiseDisjoint_Ioc rfl (hu₁ s)

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
⊢ dist (f d) (f b) ≤ y
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 :
  ∀ ε > 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
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
⊢ BoundedVariationOn f (Icc a b)

Tactic:
have v_sum : eVariationOn f (Icc a b) =
      ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + i * δ') (a + (i + 1) * δ')) := by
    convert! eVariationOn.sum' f (I := fun i ↦ a + i * δ') h_mono |>.symm
    · simp
    · simp only [Nat.cast_add, Nat.cast_one, δ']; field
    · norm_cast

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
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
⊢ BoundedVariationOn f (Icc a b)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : 1 < M
⊢ Filter.map ofReal (𝓝[<] 1) ≤ 𝓝[stolzSet M] 1

Tactic:
← tendsto_id'

Goal state after:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
inv_smul_eq_iff₀,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = ‖x‖ • ‖y‖⁻¹ • y

case ha
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ ≠ 0
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖y‖⁻¹ • ‖x‖ • y = x

pp: case ha
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
inv_smul_eq_iff₀,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x

case ha
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖y‖ ≠ 0

case ha
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ ≠ 0
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ ball z r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)
  · rw [closedBall_zero, mem_singleton_iff] at hx hy
    exact (hne (hx.trans hy.symm)).elim
  · simp only [← interior_closedBall _ hr] at hx hy ⊢
    exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab

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

Goal state before:
pp: case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε

Tactic:
let F := ∑ i ∈ range B₁, ‖l - s (i + 1)‖

Goal state after:
case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (Ioi 0) fun x ↦ x ^ m

Tactic:
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)

Goal state after:
case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x ↦ x ^ m) (Ioi 0)

case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ x ∈ Ioi 0, 0 < deriv^[2] (fun x ↦ x ^ m) x
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x ↦ x ^ m) x

Tactic:
rw [iter_deriv_zpow]

Goal state after:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i ∈ Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case h₁
x y : ℂ
⊢ (∃ k, x = ↑k * ↑π * 2 + y) ↔ ∃ k, y = ↑k * ↑π * 2 + x

Tactic:
constructor <;> · rintro ⟨k, rfl⟩; use -k; simp

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

Goal state before:
pp: case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
rcases exists_mem_frontier_infDist_compl_eq_dist hwU this with ⟨z, hzU, hzw⟩

Goal state after:
case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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
⊢ ((∀ (k : ℤ), ↑x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑y = (2 * ↑l + 1) * ↑π / 2

Tactic:
convert h <;> norm_cast

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

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

Tactic:
simpa [cos_sq_arctan] using
    tanPartialHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)

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

Goal state before:
pp: case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 2 * ↑r + 1 ≤ -1

Tactic:
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]

Goal state after:
case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ (-1 - 1) / 2

case inr
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 0 < 2
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: 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)⁻¹

Tactic:
· refine eventually_mem_nhdsWithin.mono fun w hw ↦ ?_
        rw [mem_compl_singleton_iff, ← sub_ne_zero] at hw
        simp [pow_succ, field]

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 : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
⊢ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
filter_upwards [h₁f.analyticAt_mem_codiscreteWithin,
    h₁f.codiscreteWithin_setOfPred_meromorphicOrderAt_eq_zero_or_top h₂f] with x h₁x h₂x

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
x : 𝕜
h₁x : AnalyticAt 𝕜 f x
h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)
⊢ f x ≠ 0
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 : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
⊢ ((divisor f U).restrict hV) x = (divisor f V) x

Tactic:
by_cases hx : x ∈ V

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∈ V
⊢ ((divisor f U).restrict hV) x = (divisor f V) x

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∉ V
⊢ ((divisor f U).restrict hV) x = (divisor f V) x
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 : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∈ V
⊢ ((divisor f U).restrict hV) x = (divisor f V) x

Tactic:
rw [Function.locallyFinsuppWithin.restrict_apply]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
hx : x ∈ V
⊢ (if x ∈ V then (divisor f U) x else 0) = (divisor f V) x
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
rw [show f = ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) by aesop]

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicNFAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)