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 : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)

Tactic:
have A : ∫⁻ x in e '' s, u (n x) = ∫⁻ x in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x) := by
    rw [← lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn hs hg' hf.neg (u ∘ n)]; rfl

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun x ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ x ∈ s, HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case hint
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
⊢ IntervalIntegrable f' volume (↑N) x

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]

Goal state after:
case hint
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
⊢ IntegrableOn f' (Ioc (↑N) x) volume
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case hst
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε
B : ∀ᶠ (n : ℕ) in atTop, a < ↑n
N : ℕ
hN : ∫ (x : ℝ) in Ici ↑N, ‖f' x‖ < ε
h'N : a < ↑N
x : ℝ
hx : x ≥ ↑N
this : Ioc (↑N) x ⊆ Ici ↑N
⊢ Ioc (↑N) x ≤ᵐ[volume] Ici ↑N

Tactic:
exact this.eventuallyLE

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : OpensMeasurableSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
f : E → F
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
hf : Continuous f
⊢ Measurable fun p ↦ lineDeriv 𝕜 f p.1 p.2

Tactic:
borelize 𝕜
  let g : (E × E) → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)
  have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)
  exact (measurable_deriv_with_param this).comp measurable_prodMk_right

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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ IntervalIntegrable f' volume x a

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]

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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ IntegrableOn f' (Ioc x a) volume
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
⊢ AnalyticAt ℂ f c

Tactic:
rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 hd with ⟨R, hR0, hRs⟩

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ
hR0 : 0 < R
hRs : closedBall c R ∩ {c}ᶜ ⊆ {x | (fun z ↦ DifferentiableAt ℂ f z) x}
⊢ AnalyticAt ℂ f c
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 : ℂ
hs : s ∈ 𝓝 c
⊢ DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c → DifferentiableOn ℂ f s

Tactic:
rintro ⟨hd, hc⟩ x hx

Goal state after:
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
⊢ DifferentiableWithinAt ℂ f s x
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case inl
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e ↦ e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

pp: case inr
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e ↦ e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

Tactic:
· rw [← hxe]; left; use x

Goal state after:
case inr
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
h : Nonempty H
e : OpenPartialHomeomorph (M ⊕ M') H
x : OpenPartialHomeomorph M' H
hx : x ∈ ChartedSpace.atlas
hxe : (fun e ↦ e.lift_openEmbedding ⋯) x = e
⊢ (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯
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
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst✝] s
ts : t = ↑e' ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)
⊢ ↑e' ∘ ↑e.symm ⁻¹' s ∩ e.target ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ (↑e' ∘ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source)

Tactic:
← inter_assoc

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
e' : PartialEquiv M H
e'_atlas : e' ∈ c.atlas
s : Set H
s_open : IsOpen[inst✝] s
ts : t = ↑e' ⁻¹' s ∩ e'.source
f : PartialEquiv H H := e.symm ≫ e'
this : IsOpen[inst✝] (↑f ⁻¹' s ∩ f.source)
⊢ ↑e' ∘ ↑e.symm ⁻¹' s ∩ e.target ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e' ∘ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG₁ PG₂ : Pregroupoid H
h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s
⊢ PG₁.groupoid ≤ PG₂.groupoid

Tactic:
by
  refine StructureGroupoid.le_iff.2 fun e he ↦ ?_
  rw [mem_groupoid_of_pregroupoid] at he ⊢
  exact ⟨h _ _ he.1, h _ _ he.2⟩

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 : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
by rwa [f.extend_source]

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 : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
by rwa [f.extend_source]

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 : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
e : PartialEquiv M E := f.extend I
⊢ y ∈ (f.extend I).source

Tactic:
by rwa [f.extend_source]

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

Goal state before:
pp: case pos
𝕜 : 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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
W : Convex ℝ (range ↑I)
⊢ Convex ℝ (range ↑I)

Tactic:
simp only [Convex, StarConvex] at W ⊢

Goal state after:
case pos
𝕜 : 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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
W :
  ∀ ⦃x : E⦄, x ∈ range ↑I → ∀ ⦃y : E⦄, y ∈ range ↑I → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ range ↑I
⊢ ∀ ⦃x : E⦄, x ∈ range ↑I → ∀ ⦃y : E⦄, y ∈ range ↑I → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ range ↑I
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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

Tactic:
rw [← liftPropWithinAt_indep_chart_aux' hG he' xe' hf' xf' hgs,
    liftPropWithinAt_indep_chart_aux' hG he xe hf xf hgs]

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
s : Set H
hs : IsOpen[inst✝] s
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' s ∩ range ↑I)

Tactic:
by
  rw [inter_comm]
  exact I.uniqueDiffOn.inter (hs.preimage I.continuous_invFun)

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
this : LiftPropWithinAt P g (s ∩ u) x
⊢ LiftPropWithinAt P g s x

Tactic:
rwa [hG.liftPropWithinAt_inter] at this

Goal state after:
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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
this : LiftPropWithinAt P g (s ∩ u) x
⊢ u ∈ 𝓝 x
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
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ∀ (o : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
      ↑(extChartAt I x₀) x ∈ o →
        (o ∩ (interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target)).Nonempty

Tactic:
← inter_assoc

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
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst✝¹] (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ∀ (o : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
      ↑(extChartAt I x₀) x ∈ o →
        (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
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'
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
s t : Set M
hf : ContMDiffOn I I' n f s
hf' : ContMDiffOn I I' n f t
hs : IsOpen[inst✝⁶] s
ht : IsOpen[inst✝⁶] t
⊢ ContMDiffOn I I' n f (s ∪ t)

Tactic:
intro x hx
  obtain (hx | hx) := hx
  · exact (hf x hx).contMDiffAt (hs.mem_nhds hx) |>.contMDiffWithinAt
  · exact (hf' x hx).contMDiffAt (ht.mem_nhds hx) |>.contMDiffWithinAt

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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
M' : Type u_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))

Tactic:
let hg' := hg x

Goal state after:
𝕜 : 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
M' : Type u_16
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝² : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
hg' : ContMDiffAt I J n g x := hg x
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: case refine_1.hf
𝕜 : 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
M' : Type u_7
inst✝ : TopologicalSpace M'
f : M → M'
s : Set M
x : M
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
exact (continuousAt_extChartAt_symm x).continuousWithinAt

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

Goal state before:
pp: case right
𝕜 : 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 : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
this : IsManifold I ω M
⊢ ∀ (x : M) (y : H),
    ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' e ⁻¹' (extChartAt I y).source)

Tactic:
intro x y

Goal state after:
case right
𝕜 : 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 : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
⊢ ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ e ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' e ⁻¹' (extChartAt I y).source)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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
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'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
h : ContinuousOn f s
⊢ ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 0 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
intro x y

Goal state after:
𝕜 : 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
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'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
h : ContinuousOn f s
x : M
y : M'
⊢ ContDiffOn 𝕜 0 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

Goal state before:
pp: case inr
𝕜 : 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
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'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
this : ∀ {s : Set M}, x ∈ s → (ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u)
hxs : x ∉ s
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

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
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'
inst✝² : ChartedSpace H' M'
f : M → M'
s✝ : Set M
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

Tactic:
· rw [← contMDiffWithinAt_insert_self, this (mem_insert _ _), insert_idem]

Goal state after:
𝕜 : 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
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'
inst✝² : ChartedSpace H' M'
f : M → M'
s✝ : Set M
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : Mul G
inst✝¹ : TopologicalSpace G
inst✝ : ChartedSpace H G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffMul I n G
⊢ ContMDiffMul I m G

Tactic:
have : IsManifold I m G := IsManifold.of_le hmn

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝² : Mul G
inst✝¹ : TopologicalSpace G
inst✝ : ChartedSpace H G
m n : ℕ∞ω
hmn : m ≤ n
h : ContMDiffMul I n G
this : IsManifold I m G
⊢ ContMDiffMul I m G