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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := ⋯
a_count : a.Countable
s₁ : Set ℝ := ⋯
hs₁ : MeasurableSet s₁
u : Set ℝ := ⋯
hu : u.Countable
b : Set ℝ := ⋯
hb : MeasurableSet b
c : Set ℝ := ⋯
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
⊢ UniqueDiffWithinAt ℝ (s ∩ Ioo x p) x

Tactic:
have J1 : (s ∩ Ioo x p) \ {x} = (s ∩ Ioo x p) := by simp

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
K : HasDerivWithinAt f 0 (s ∩ Ioo x p) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo x p) x
J1 : (s ∩ Ioo x p) \ {x} = s ∩ Ioo x p
⊢ UniqueDiffWithinAt ℝ (s ∩ Ioo x p) x
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
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right

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
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
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
⊢ IntegrableOn g (f '' c) volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume

Tactic:
have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right

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
⊢ 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
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)

Tactic:
have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right

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
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i ↦ Ioc (a i) (b i)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
⊢ ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I

Tactic:
ht

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i ↦ Ioc (a i) (b i)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Iic (b i)
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))

Tactic:
have hφ : AECover (μ.restrict <| Ioi a) l φ := aecover_Iic hb

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
⊢ atTop.limUnder (⇑F ∘ f) = F 0

Tactic:
have : IntegrableAtFilter (F ∘ f) atTop := by exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
⊢ atTop.limUnder (⇑F ∘ f) = F 0
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ (t ∈ tsupport fun x_1 ↦ g (x, x_1)) → HasDerivAt (fun x_1 ↦ f (x, x_1)) (f' (x, t)) t

Tactic:
ht

Goal state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume
t : ℝ
ht : t ∈ tsupport fun x_1 ↦ g (x, x_1)
⊢ HasDerivAt (fun x_1 ↦ f (x, x_1)) (f' (x, t)) t
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ (t ∈ tsupport fun x_1 ↦ f (x, x_1)) → HasDerivAt (fun x_1 ↦ g (x, x_1)) (g' (x, t)) t

Tactic:
ht

Goal state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume
t : ℝ
ht : t ∈ tsupport fun x_1 ↦ f (x, x_1)
⊢ HasDerivAt (fun x_1 ↦ g (x, x_1)) (g' (x, t)) t
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
hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
exact (hderiv a self_mem_Ici).continuousAt.continuousWithinAt

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

Goal state before:
pp: case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Tactic:
hasCompactSupport_iff_eventuallyEq,

Goal state after:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[coclosedCompact ℝ] 0
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact (hderiv a self_mem_Ici).continuousAt.continuousWithinAt

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

Goal state before:
pp: g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact (hderiv a self_mem_Ici).continuousAt.continuousWithinAt

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

Goal state before:
pp: case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

Tactic:
hasCompactSupport_iff_eventuallyEq,

Goal state after:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[coclosedCompact ℝ] 0
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: case pos
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
x : E
hx : x ∈ tsupport g
⊢ (B (f' x)) (g x) = 0

Tactic:
simp [(hasLineDerivAt_zero (f := f) (x := x)).lineDeriv, (hf x hx).lineDeriv.symm]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝² : CommMonoid α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
h2 : MultipliableLocallyUniformlyOn f s
⊢ MultipliableLocallyUniformlyOn f' s

Tactic:
apply HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
  exact (h2.hasProdLocallyUniformlyOn).congr fun v ↦ eqOn_fun_finsetProd h v

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

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
⊢ t ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen[inst✝] s), {↑e ⁻¹' s ∩ e.source} → IsOpen[inst✝] (e.target ∩ e.invFun ⁻¹' t)

Tactic:
ht

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e✝ e : PartialEquiv M H
he : e ∈ c.atlas
this : TopologicalSpace M := c.toTopologicalSpace
t : Set M
ht : t ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen[inst✝] s), {↑e ⁻¹' s ∩ e.source}
⊢ IsOpen[inst✝] (e.target ∩ e.invFun ⁻¹' t)
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case right.refine_2
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}
⊢ PG.property (↑e.symm) (e.target ∩ (e.target ∩ ↑e.symm ⁻¹' s))

Tactic:
rw [← inter_assoc, inter_self]

Goal state after:
case right.refine_2
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}
⊢ PG.property (↑e.symm) (e.target ∩ ↑e.symm ⁻¹' s)
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case left
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ PG.property (↑e') e'.source

pp: case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ PG.property (↑e'.symm) e'.target

Tactic:
· apply PG.congr e'.open_source ee'.2
      simp only [ee'.1, he.1]

Goal state after:
case right
H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he : e ∈ {e | PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target}
ee' : e' ≈ e
⊢ PG.property (↑e'.symm) e'.target
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f g : H → H'
hu : s =ᶠ[𝓝 x] t
h : f =ᶠ[𝓝 x] g
⊢ P f s x ↔ P g t x

Tactic:
by
  rw [hG.congr_iff h, hG.congr_set hu]

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
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ T1Space M

Tactic:
by
  have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space
  exact ChartedSpace.t1Space H M

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
⊢ t ∈ 𝓝 y → (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
ht

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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty
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
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
h''z : z ∈ (extChartAt I x).target
⊢ z ∈ interior (extChartAt I x).target

Tactic:
exact (extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑e x))
hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)
A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source
x' : E
hfx' : f (↑e.symm x') ∈ e'.source
⊢ (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) x' =
    ((↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) ∘ writtenInExtChartAt I I' x f) x'

Tactic:
simp only [*, e, e', (· ∘ ·), writtenInExtChartAt, e'.left_inv]

Goal state after: