mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
          ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∑ i_1 ∈ Finset.range (n + 1),
      ↑(n.choose i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y ↦ ∏ i ∈ u, f i y) s x‖ ≤
    ∑ i_1 ∈ Finset.univ.sigma fun x ↦ Finset.univ,
      ((fun v ↦ ↑v.countPerms * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
        i_1

Tactic:
Finset.sum_sigma,

Goal state after:
case insert
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
          ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∑ i_1 ∈ Finset.range (n + 1),
      ↑(n.choose i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y ↦ ∏ i ∈ u, f i y) s x‖ ≤
    ∑ a,
      ∑ s_1,
        ((fun v ↦ ↑v.countPerms * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
            Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
          ⟨a, s_1⟩
Module: Mathlib.Analysis.Calculus.FDeriv.Star

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : StarRing 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : StarModule 𝕜 F
inst✝⁴ : ContinuousStar F
inst✝³ : StarAddMonoid E
inst✝² : StarModule 𝕜 E
inst✝¹ : ContinuousStar E
inst✝ : NormedStarGroup 𝕜
f : E → F
z : E
f' : E →L[𝕜] F
hf : HasFDerivAt f f' z
⊢ HasFDerivAt f f' (↑(starL 𝕜) (star z))

Tactic:
simpa using hf

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
⊢ ↑i + 1 ≤ ↑(n + 1)

Tactic:
Nat.cast_succ,

Goal state after:
case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
⊢ ↑i + 1 ≤ ↑n + 1
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ Tendsto (fun n ↦ (↑N / (↑N + 1)) ^ n * μ s) atTop (𝓝 (0 * μ s))

Tactic:
apply ENNReal.Tendsto.mul_const _ (Or.inr (measure_lt_top μ s).ne)

Goal state after:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop := ⋯
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := ⋯
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ Tendsto (HPow.hPow (↑N / (↑N + 1))) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ ↑N + 0 < ↑N + 1

Tactic:
exact ENNReal.add_lt_add_left (ENNReal.natCast_ne_top N) zero_lt_one

Goal state after:
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
r : WithTop ℕ∞
ω : E → E [⋀^Fin n]→L[𝕜] F
s : Set E
x : E
hω : ContDiffWithinAt 𝕜 r ω s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
⊢ 1 + 1 ≤ r

Tactic:
exact le_minSmoothness.trans hr

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x | (fun y ↦ HasFDerivAt f (f' y) y) x}
A : (interior (Metric.ball x ε)).Nonempty
⊢ (f'' v) w = (f'' w) v

Tactic:
exact
    Convex.second_derivative_within_at_symmetric (convex_ball x ε) A
      (fun y hy => hε (interior_subset hy)) (Metric.mem_ball_self εpos) hx.hasFDerivWithinAt v w

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace 𝕜
z₀ : 𝕜
R R₁ : 𝕜 → 𝕜
hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z
k : ℕ
IH :
  ∀ {t : ℕ},
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t)! / ↑t ! * R₁ z + (z - z₀) * R₂ z)
t : ℕ
hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + 1 + t) * R₁ z
R₂ : 𝕜 → 𝕜
hR₂ : ∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z
hR₂_eq : ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z)
R₂' : 𝕜 → 𝕜 := fun z ↦ (↑t + 1) * R₂ z + (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
z : 𝕜
⊢ deriv (fun w ↦ (w - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ w + (w - z₀) * R₂ w)) z =
    (↑t + 1) * (z - z₀) ^ t * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z) +
      (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))

Tactic:
have hsub : HasDerivAt (· - z₀) 1 z := (hasDerivAt_id z).sub_const z₀

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace 𝕜
z₀ : 𝕜
R R₁ : 𝕜 → 𝕜
hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z
k : ℕ
IH :
  ∀ {t : ℕ},
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t)! / ↑t ! * R₁ z + (z - z₀) * R₂ z)
t : ℕ
hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + 1 + t) * R₁ z
R₂ : 𝕜 → 𝕜
hR₂ : ∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z
hR₂_eq : ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z)
R₂' : 𝕜 → 𝕜 := fun z ↦ (↑t + 1) * R₂ z + (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
z : 𝕜
hsub : HasDerivAt (fun x ↦ x - z₀) 1 z
⊢ deriv (fun w ↦ (w - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ w + (w - z₀) * R₂ w)) z =
    (↑t + 1) * (z - z₀) ^ t * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z) +
      (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : 0 < x
⊢ ((fun x ↦ f' x / g' x) ∘ fun x ↦ x⁻¹) x = f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)

Tactic:
simp only [Function.comp_def]

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : 0 < x
⊢ f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
⊢ Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ⋯
HC : IsCompact (⇑A '' closedBall 0 1)
⊢ Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)
J : ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)
⊢ Tendsto (fun a ↦ ↑m * (μ s + a)) (𝓝[>] 0) (𝓝 (↑m * (μ s + 0)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ⋯
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)
J : ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)
⊢ Tendsto (fun a ↦ ↑m * (μ s + a)) (𝓝 0) (𝓝 (↑m * (μ s + 0)))
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x

Tactic:
have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ ∫ (x : ℝ) in Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : ‖w - z‖ = r
h : (w - z) ^ 2 = 0
⊢ 0 = r

Tactic:
sq_eq_zero_iff.mp h,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : ‖0‖ = r
h : (w - z) ^ 2 = 0
⊢ 0 = r
Module: Mathlib.Analysis.RCLike.TangentCone

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hs : UniqueDiffWithinAt ℝ s x
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
by
  let := h𝕜.rclike
  exact hs.mono_field

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
hs : IsOpen[inst✝²] s
xs : x ∈ s
A : e.symm ≫ₕ f ∈ G
B : f.symm ≫ₕ e' ∈ G
C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G
⊢ (e.symm ≫ₕ ofSet f.source ⋯) ≫ₕ e' ≈ e.symm.restr s ≫ₕ e'

Tactic:
rw [trans_of_set']; apply refl

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

Goal state before:
pp: case e'_5
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst✝] s
xs : x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e.source ∩ s = (e.restr s).source

Tactic:
dsimp [OpenPartialHomeomorph.restr]

Goal state after:
case e'_5
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.source
s : Set H
s_open : IsOpen[inst✝] s
xs : x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e.source ∩ s = e.source ∩ interior s
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case e'_5
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e.target ∩ ↑e.symm ⁻¹' s = (e.restr s).target

Tactic:
dsimp [OpenPartialHomeomorph.restr]

Goal state after:
case e'_5
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
x : H
xu : x ∈ e.target
s : Set H
s_open : IsOpen[inst✝] s
xs : ↑e.symm x ∈ s
hs : e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ ↑e.symm ⁻¹' interior s
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e : OpenPartialHomeomorph H H
he :
  ∀ x ∈ e.source,
    ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
⊢ e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}

Tactic:
by
    constructor
    · refine PG.locality e.open_source fun x xu ↦ ?_
      rcases he x xu with ⟨s, s_open, xs, hs⟩
      refine ⟨s, s_open, xs, ?_⟩
      convert! hs.1 using 1
      dsimp [OpenPartialHomeomorph.restr]
      rw [s_open.interior_eq]
    · refine PG.locality e.open_target fun x xu ↦ ?_
      rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩
      refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩
      · exact ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open
      · rw [← inter_assoc, inter_self]
        convert! hs.2 using 1
        dsimp [OpenPartialHomeomorph.restr]
        rw [s_open.interior_eq]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ Tendsto (fun ε ↦ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0)
    (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑0 * μ s))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ Tendsto (fun ε ↦ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝 0)
    (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑0 * μ s))
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst✝] (f.source ∩ ↑(f.extend I) ⁻¹' s)

Tactic:
rw [← extend_source f (I := I)]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst✝] ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case hu.refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ x ∈ (chartAt H x).source

Tactic:
mem_chart_source H x

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

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
x : H
s : Set H
⊢ map (↑I.symm) (𝓝[↑I '' s] ↑I x) = 𝓝[s] x

Tactic:
by
  rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ (extChartAt I x).target ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
by
  convert! extChartAt_target_mem_nhdsWithin x
  simp only [I.range_eq_univ, nhdsWithin_univ]

Goal state after: