mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
let F' : ℝ → (ℝ →L[ℝ] ℝ) := fun x ↦ ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
by
  rw [eventually_iff_exists_mem] at *
  rcases hff' with ⟨s₁, hs₁, hff'⟩
  rcases hgg' with ⟨s₂, hs₂, hgg'⟩
  rcases hg' with ⟨s₃, hs₃, hg'⟩
  let s := s₁ ∩ s₂ ∩ s₃
  have hs : s ∈ atBot := inter_mem (inter_mem hs₁ hs₂) hs₃
  rw [mem_atBot_sets] at hs
  rcases hs with ⟨l, hl⟩
  have hl' : Iio l ⊆ s := fun x hx => hl x (le_of_lt hx)
  refine lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hfbot hgbot hdiv <;> grind

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
by
  refine derivWithin.lhopital_zero_nhdsWithin_convex hs
    (hdf.mono fun _ h ↦ h.differentiableWithinAt) (hg'.mp ?_) hfa hga
    (hdiv.congr' ?_)
  all_goals
    apply (hs.sdiff_singleton_eventually_mem_nhds a).mono
    intros
  · rwa [derivWithin_of_mem_nhds ‹_›]
  · simp only
    iterate 2 rw [derivWithin_of_mem_nhds ‹_›]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
c_s : c ⊆ s
⊢ IntegrableOn g (f '' c) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume

Tactic:
let F' : ℝ → (ℝ →L[ℝ] ℝ) := fun x ↦ ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
⊢ IntegrableOn g (f '' c) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
J : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in f '' c, g x
⊢ ∫ (x : ℝ) in f '' c, g x = ∫ (x : ℝ) in c, f' x • g (f x)

Tactic:
let F' : ℝ → (ℝ →L[ℝ] ℝ) := fun x ↦ ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)

Goal state after:
case pos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
g : ℝ → F
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
J : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in f '' c, g x
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
⊢ ∫ (x : ℝ) in f '' c, g x = ∫ (x : ℝ) in c, f' x • g (f x)
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δ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
⊢ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = ⇑A '' closedBall 0 (|r| * 1) + closedBall (f x) (|r| * ε)

Tactic:
abs_of_nonneg r0,

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∞ := 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δ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
⊢ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = ⇑A '' closedBall 0 (r * 1) + closedBall (f x) (r * ε)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf'
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
⊢ DifferentiableOn ℝ f (interior (Icc a b))

pp: case hf'_nonneg
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x

Tactic:
· rw [interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Goal state after:
case hf'_nonneg
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf'_nonneg
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x

Tactic:
· rw [interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz

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

Goal state before:
pp: case hf'
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
⊢ DifferentiableOn ℝ f (interior (Icc a b))

pp: case hf'_nonpos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0

Tactic:
· rw [interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Goal state after:
case hf'_nonpos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf'_nonpos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0

Tactic:
· rw [interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))

Tactic:
apply Tendsto.congr' _ (hf.sub_const _)

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
⊢ (fun x ↦ f x - f a) =ᶠ[atTop] fun i ↦ ∫ (x : ℝ) in a..id i, f' x
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
⊢ b • ∫ (x : ℝ) in Ioi a, g (x * b) = ∫ (x : ℝ) in Ioi (a * b), g x

Tactic:
by
  simp [integral_comp_mul_right_Ioi g a hb, smul_smul, mul_inv_cancel₀ hb.ne']

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

Goal state before:
pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
hne : x ≠ c
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
simpa only [DifferentiableWithinAt, HasFDerivWithinAt, hne.nhdsWithin_sdiff_singleton] using
      hd x ⟨hx, hne⟩

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
F : ℂ → E := fun z ↦ (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x ↦ (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update f c ((𝓝[≠] c).limUnder f)) s

Tactic:
have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
      continuousAt_update_same.mp (this.continuousOn.continuousAt hc)

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
F : ℂ → E := fun z ↦ (z - c) • f z
this : DifferentiableOn ℂ (update f c (deriv (fun x ↦ (x - c) • f x) c)) s
hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c ((𝓝[≠] c).limUnder f)) s
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' : Integrable (fun x ↦ (L (u x)) (v' x)) volume
hu'v : Integrable (fun x ↦ (L (u' x)) (v x)) volume
huv : Integrable (fun x ↦ (L (u x)) (v x)) volume
hG : CompleteSpace G
I : Tendsto (fun x ↦ (L (u x)) (v x)) atBot (𝓝 0)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
have J : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0)
      (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
      (huv'.add hu'v).integrableOn huv.integrableOn

Goal state after:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' : Integrable (fun x ↦ (L (u x)) (v' x)) volume
hu'v : Integrable (fun x ↦ (L (u' x)) (v x)) volume
huv : Integrable (fun x ↦ (L (u x)) (v x)) volume
hG : CompleteSpace G
I : Tendsto (fun x ↦ (L (u x)) (v x)) atBot (𝓝 0)
J : Tendsto (fun x ↦ (L (u x)) (v x)) atTop (𝓝 0)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v 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)
h1 : ContinuousOn (fun w ↦ ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z

Tactic:
cderiv,

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)
h1 : ContinuousOn (fun w ↦ ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ (2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w =
    ((2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) -
      (2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: case inr
E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε

Tactic:
filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz

Goal state after:
E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h : ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε * δ
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
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
⊢ (f.extend I).target = ↑(f.extend I) '' f.source

Tactic:
rw [f.extend_target', ← f.image_source_eq_target, ← image_comp, f.extend_coe]

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

Goal state before:
pp: case neg
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁸ : TopologicalSpace H
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : TopologicalSpace M''
G : StructureGroupoid H
inst✝³ : ChartedSpace H M'
inst✝² : ChartedSpace H M''
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
h : IsEmpty ↑e.source
⊢ Structomorph G ↥s ↥t

Tactic:
have : IsEmpty t := isEmpty_coe_sort.mpr
      (by convert! e.image_source_eq_target ▸ image_eq_empty.mpr (isEmpty_coe_sort.mp h))
    exact { Homeomorph.empty with
      -- `c'` cannot exist: it would be the restriction of `chartAt H x` at some `x ∈ t`.
      mem_groupoid := fun _ c' _ ⟨_, ⟨x, _⟩, _⟩ ↦ (this.false x).elim }

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

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ LiftProp P f ↔
    Continuous[inst✝⁴, inst✝¹] f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
by
  simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]

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
f f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑(f.extend I) '' (f.source ∩ f'.source) = (extendCoordChange f f').source

Tactic:
I.extendCoordChange_source,

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 f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑(f.extend I) '' (f.source ∩ f'.source) = ↑I '' (f.symm ≫ₕ f').source
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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange e e')) (extendCoordChange e e').source

Tactic:
I.extendCoordChange_source,

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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange e e')) (↑I '' (e.symm ≫ₕ e').source)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type w
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝⁴ : I.Boundaryless
E' : Type v'
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H' : Type w'
inst✝¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst✝ : I'.Boundaryless
⊢ univ ×ˢ univ = univ

Tactic:
univ_prod_univ

Goal state after:
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type w
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝⁴ : I.Boundaryless
E' : Type v'
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H' : Type w'
inst✝¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst✝ : I'.Boundaryless
⊢ univ = univ
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : 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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid n I

Tactic:
by
  constructor
  · intro x ⟨hx, _⟩
    rw [mem_preimage] at hx
    simp_all only [mem_empty_iff_false]
  · intro x ⟨hx, _⟩
    have : f.target = ∅ := by simp [← f.image_source_eq_target, hf]
    simp_all

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

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : ↑e' x ∈ ↑e'.symm ⁻¹' s
⊢ ∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source

Tactic:
have hxs : x ∈ s := by simpa only [e'.left_inv he'x, mfld_simps] using hx

Goal state after:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : ↑e' x ∈ ↑e'.symm ⁻¹' s
hxs : x ∈ s
⊢ ∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source