mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝¹ : x ∈ s
e : OpenPartialHomeomorph X Y
hx✝ : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_x : X
hx : _x ∈ e.source
⊢ f _x ∈ e.target

Tactic:
by rw [he hx]; exact e.map_source' hx

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsLocalHomeomorphOn f Set.univ ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)

Tactic:
isLocalHomeomorphOn_iff_isOpenEmbedding_restrict,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ x ∈ Set.univ, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)) ↔
    ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
hxf : ↑x ∉ Set.range f
U : Set X
hUx : U ∈ 𝓝 ↑x
hfU : f ⁻¹' U = ∅
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑x})

Tactic:
exact .to_isEvenlyCovered_preimage (.of_preimage_eq_empty Empty hUx hfU)

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

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ (↑(↑z).arg).toReal ∈ Ioo (-(π / ↑n)) (π / ↑n)

Tactic:
mem_Ioo,

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ -(π / ↑n) < (↑(↑z).arg).toReal ∧ (↑(↑z).arg).toReal < π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x : AddCircle T
n : ℕ
⊢ (n • x).toCircle = x.toCircle ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ spectrum ℂ ↑(expUnitary x) ⊆ slitPlane

Tactic:
spectrum_subset_slitPlane_iff_norm_lt_two (expUnitary x).2,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ ‖↑(expUnitary x) - 1‖ < 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
⊢ z ∈ centeredArc (π / 2 ^ (n + 1))

Tactic:
induction n with

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

Goal state before:
pp: case refine_2
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ (⇑e ⁻¹' ↑(zpowGroupHom n).ker).Finite

Tactic:
· convert! finite_torsion_of_isSMulRegular_int (1 : ℝ) n fun _ ↦ by simp [NeZero.ne]
    ext
    simp [e, homeomorphCircle_apply, ← toCircle_zsmul, ← (injective_toCircle one_ne_zero).eq_iff]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a

Tactic:
CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfcₙ Real.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a

case nonneg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ 0 ≤ 1 - a ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ‖x.re‖ ≤ 1

Tactic:
exact spectrum.norm_le_norm_of_mem (ha.spectrumRestricts.apply_mem hx) |>.trans ha_norm

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
⊢ IsSelfAdjoint T ↔ IsStarNormal T

Tactic:
by
  refine ⟨fun h => by rw [isStarNormal_iff, h], fun h => ?_⟩
  suffices T = star T * T from this ▸ IsSelfAdjoint.star_mul_self _
  rw [← sub_eq_zero, ContinuousLinearMap.ext_iff]
  simp_rw [zero_apply, ← norm_eq_zero (E := E)]
  have :=
    calc (∀ x : E, ‖(T - star T * T) x‖ = 0) ↔ ∀ x, ‖(adjoint (1 - T)) (T x)‖ = 0 := by
          simp [star_eq_adjoint, one_def]
      _ ↔ ∀ x, ‖(1 - T) (T x)‖ = 0 := by
          simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]
      _ ↔ ∀ x, ‖(T - T * T) x‖ = 0 := by simp
      _ ↔ T - T * T = 0 := by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]
      _ ↔ IsIdempotentElem T := by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]
  exact this.mpr hT

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ (adjoint T ∘ₗ T).IsSymmetric

Tactic:
by
  simpa using LinearMap.IsSymmetric.id.adjoint_conj T

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ t
hps : p ∈ s
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, hp⟩ ∈ u

Tactic:
simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one]

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ t
hps : p ∈ s
⊢ p ∈ u
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ t
hps : p ∉ s
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, hp⟩ ∈ u

Tactic:
simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one]

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ t
hps : p ∉ s
⊢ (lineMap q p) (ε / dist p q) ∈ u
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ Memℓp (f + g) ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Memℓp (f + g) p

Tactic:
· apply memℓp_infty
    obtain ⟨A, hA⟩ := hf.bddAbove
    obtain ⟨B, hB⟩ := hg.bddAbove
    refine ⟨A + B, ?_⟩
    rintro a ⟨i, rfl⟩
    exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Memℓp (f + g) p
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ⇑((Homeomorph.smulOfNeZero r ⋯).trans (IsometryEquiv.vaddConst c).toHomeomorph) '' ball 0 1 = ball c r

Tactic:
change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r
    rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
    simp [abs_of_pos hr]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ Tendsto (id fun i ↦ ↑((fun f ↦ F n - f) (F i))) atTop (𝓝 ↑(F n - f))

Tactic:
rw [tendsto_pi_nhds]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ ∀ (x : α), Tendsto (fun i ↦ id (fun i ↦ ↑((fun f ↦ F n - f) (F i))) i x) atTop (𝓝 (↑(F n - f) x))
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
  have : NeBot l := (cauchy_map_iff.1 hfg).1
  rcases le_or_gt r 0 with (hr | hr)
  · simp only [Metric.ball_eq_empty.2 hr, UniformCauchySeqOn, Set.mem_empty_iff_false,
      IsEmpty.forall_iff, eventually_const, imp_true_iff]
  rw [SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero] at hf' ⊢
  suffices
    TendstoUniformlyOn (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
        (l ×ˢ l) (Metric.ball x r) ∧
      TendstoUniformlyOn (fun (n : ι × ι) (_ : E) => f n.1 x - f n.2 x) 0
        (l ×ˢ l) (Metric.ball x r) by
    have := this.1.neg.add this.2.neg
    rw [neg_zero, add_zero] at this
    refine this.congr ?_
    filter_upwards with n z _ using (by simp; abel)
  constructor
  · -- This inequality follows from the mean value theorem
    rw [Metric.tendstoUniformlyOn_iff] at hf' ⊢
    intro ε hε
    obtain ⟨q, hqpos, hq⟩ : ∃ q : ℝ, 0 < q ∧ q * r < ε := by
      simp_rw [mul_comm]
      exact exists_pos_mul_lt hε.lt r
    apply (hf' q hqpos.gt).mono
    intro n hn y hy
    simp_rw [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg, norm_neg_add] at hn ⊢
    have mvt :=
      Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
        (fun z hz => ((hf n.1 z hz).sub (hf n.2 z hz)).hasFDerivWithinAt) (fun z hz => (hn z hz).le)
        (convex_ball x r) (Metric.mem_ball_self hr) hy
    refine lt_of_le_of_lt mvt ?_
    have : q * ‖y - x‖ < q * r :=
      mul_lt_mul' rfl.le (by simpa only [dist_eq_norm] using Metric.mem_ball.mp hy) (norm_nonneg _)
        hqpos
    exact this.trans hq
  · -- This is just `hfg` run through `eventually_prod_iff`
    refine Metric.tendstoUniformlyOn_iff.mpr fun ε hε => ?_
    obtain ⟨t, ht, ht'⟩ := (Metric.cauchy_iff.mp hfg).2 ε hε
    rw [eventually_prod_iff]
    refine ⟨fun n => f n x ∈ t, ht, fun n => f n x ∈ t, ht, ?_⟩
    intro n hn n' hn' z _
    rw [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg, ← dist_eq_norm]
    exact ht' _ hn _ hn'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case inr.inr
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt (((fun x ↦ Polynomial.eval x p) * fun x ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (derivative p) * rexp (-x⁻¹) + Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ HasDerivAt (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue x) x

Tactic:
convert! this.congr_of_eventuallyEq _ using 1

Goal state after:
case e'_9
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt (((fun x ↦ Polynomial.eval x p) * fun x ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (derivative p) * rexp (-x⁻¹) + Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * expNegInvGlue x =
    (Polynomial.eval x⁻¹ (derivative p) * rexp (-x⁻¹) + Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹

case inr.inr.convert_2
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt (((fun x ↦ Polynomial.eval x p) * fun x ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ (derivative p) * rexp (-x⁻¹) + Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) * -(x ^ 2)⁻¹) x
⊢ (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x]
    ((fun x ↦ Polynomial.eval x p) * fun x ↦ rexp (-x)) ∘ Inv.inv
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
⊢ HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 ↿g (q₀.1, x)) q₀.2) q₀

Tactic:
have g'_zero : ∀ p x, p ∈ s → x ∉ k → g' (p, x) = 0 := by
    intro p x hp hx
    refine (hasFDerivAt_zero_of_eventually_const 0 ?_).fderiv
    have M2 : kᶜ ∈ 𝓝 x := hk.isClosed.isOpen_compl.mem_nhds hx
    have M1 : s ∈ 𝓝 p := hs.mem_nhds hp
    rw [nhds_prod_eq]
    filter_upwards [prod_mem_prod M1 M2]
    rintro ⟨p, y⟩ ⟨hp, hy⟩
    exact hgs p y hp hy

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
⊢ HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 ↿g (q₀.1, x)) q₀.2) q₀
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
x₀ : H
s : Set H
inst✝ : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x ↦ F x t) (F' t) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
  rw [ae_restrict_uIoc_iff] at h_lip h_diff
  have H₁ :=
    hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas.1 hF_int.1 hF'_meas.1 h_lip.1
      bound_integrable.1 h_diff.1
  have H₂ :=
    hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas.2 hF_int.2 hF'_meas.2 h_lip.2
      bound_integrable.2 h_diff.2
  exact ⟨⟨H₁.1, H₂.1⟩, H₁.2.sub H₂.2⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
r' : ℝ
hyr' : dist y x < r'
hrr' : r' < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ s)
B : u ∩ μ.everywherePosSubset s =ᵐ[μ] u ∩ s
⊢ 0 < μ n

Tactic:
← B.measure_eq

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ μ.everywherePosSubset s)
B : u ∩ μ.everywherePosSubset s =ᵐ[μ] u ∩ s
⊢ 0 < μ n
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ s)
B : u ∩ μ.everywherePosSubset s =ᵐ[μ] u ∩ s
⊢ 0 < μ n

Tactic:
← B.measure_eq

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
x : α
hx : x ∈ μ.everywherePosSubset s
n : Set α
hn : n ∈ 𝓝[μ.everywherePosSubset s] x
u : Set α
u_mem : u ∈ 𝓝 x
hu : u ∩ μ.everywherePosSubset s ⊆ n
A : 0 < μ (u ∩ μ.everywherePosSubset s)
B : u ∩ μ.everywherePosSubset s =ᵐ[μ] u ∩ s
⊢ 0 < μ n
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ 0 < μ (ball c f.rOut)

Tactic:
exact measure_ball_pos μ c f.rOut_pos

Goal state after: