mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: 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
k : ℕ
α : ↑I
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
x : E
hfx : ContDiffAt ℝ (↑k) f x
hgx : ContDiffAt ℝ (↑k) g x
⊢ ∀ (x_1 : Fin k → E),
    (iteratedFDeriv ℝ k (fun x ↦ (f x, g x)) x - iteratedFDeriv ℝ k (fun x ↦ (f x, g x)) a) x_1 =
      ((iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a).prod (iteratedFDeriv ℝ k g x - iteratedFDeriv ℝ k g a)) x_1

Tactic:
iteratedFDeriv_prodMk _ _ le_rfl,

Goal state after:
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
k : ℕ
α : ↑I
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
x : E
hfx : ContDiffAt ℝ (↑k) f x
hgx : ContDiffAt ℝ (↑k) g x
⊢ ∀ (x_1 : Fin k → E),
    ((iteratedFDeriv ℝ k f x).prod (iteratedFDeriv ℝ k g x) - iteratedFDeriv ℝ k (fun x ↦ (f x, g x)) a) x_1 =
      ((iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a).prod (iteratedFDeriv ℝ k g x - iteratedFDeriv ℝ k g a)) x_1

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
k : ℕ
α : ↑I
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
x : E
hfx : ContDiffAt ℝ (↑k) f x
hgx : ContDiffAt ℝ (↑k) g x
⊢ ContDiffAt ℝ (↑k) f x

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
k : ℕ
α : ↑I
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
x : E
hfx : ContDiffAt ℝ (↑k) f x
hgx : ContDiffAt ℝ (↑k) g x
⊢ ContDiffAt ℝ (↑k) g x
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r

Tactic:
apply hf.edist_le_of_le hx hy

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist x y ≤ ↑d
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 (W + W₁) x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))

Tactic:
rw [fderiv_add hW hW₁, add_apply]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W₁ x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case h₂
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
t : ℝ
ht : t ∈ Ico 0 1
I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖)
⊢ t * (h * ‖w‖) ≤ h * ‖w‖

Tactic:
exact mul_le_of_le_one_left (by positivity) ht.2.le

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x ↦ if h : x ∈ U then Exists.choose h else M
eN : (fun y ↦ ↑(N y)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x
hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x
v : E
A' : ∀ (y : E), ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm = ContinuousLinearMap.id 𝕜 F
⊢ (fderivWithin 𝕜 (fun y ↦ ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm) s x) v = 0

Tactic:
simp [A', fderivWithin_const_apply]

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

Goal state before:
pp: case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
ht : t ≠ 0
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x

Tactic:
(hd.hasFDerivAt.hasFDerivAt_norm_smul ht).fderiv

Goal state after:
case pos.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h✝ : Nontrivial E
hd : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
ht : t ≠ 0
⊢ ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E := ⋯
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
⊢ Tendsto a atTop (𝓝[s] x)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ a_lim

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E := ⋯
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
⊢ ∀ᶠ (x : ℕ) in atTop, a x ∈ s
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 : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun i ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I

Tactic:
exact id

Goal state after:
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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun i ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I

Tactic:
exact id

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → ‖(f' x - A) z‖ ≤ (↑δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
⊢ ‖(f' x - A) z‖ ≤ ↑δ * ‖z‖

Tactic:
have :
      Tendsto (fun ε : ℝ => ((δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0)
        (𝓝 ((δ + 0) * (‖z‖ + 0) + ‖f' x - A‖ * 0)) :=
      Tendsto.mono_left (Continuous.tendsto (by fun_prop) 0) nhdsWithin_le_nhds
    simp only [add_zero, mul_zero] at this
    apply le_of_tendsto_of_tendsto tendsto_const_nhds this
    filter_upwards [self_mem_nhdsWithin]
    exact H

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

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
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 : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
⊢ c ∈ atlas H M' → c' ∈ atlas H M → c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
hc

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
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 : Structomorph G M M'
c : OpenPartialHomeomorph M' H
c' : OpenPartialHomeomorph M H
hc : c ∈ atlas H M'
⊢ c' ∈ atlas H M → c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

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
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 : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
⊢ c ∈ atlas H M → c' ∈ atlas H M'' → c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
hc

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
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 : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
⊢ c' ∈ atlas H M'' → c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c' ∈ G
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
⊢ ∀ (e e' : OpenPartialHomeomorph H H),
    e ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h} →
      e' ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h} →
        e ≫ₕ e' ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h}

Tactic:
rintro e e' ⟨s, hs, hse⟩ ⟨s', hs', hse'⟩
    refine ⟨s ∩ s', hs.inter hs', ?_⟩
    have := OpenPartialHomeomorph.EqOnSource.trans' hse hse'
    rwa [OpenPartialHomeomorph.ofSet_trans_ofSet] at this

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

Goal state before:
pp: case hd
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ Pairwise (Disjoint on fun n ↦ s ∩ u n)

Tactic:
exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

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
hs : s ⊆ f.source
⊢ ↑I ∘ ↑f '' s ⊆ ↑I '' ↑f.symm ⁻¹' s

Tactic:
image_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I '' ↑f '' s ⊆ ↑I '' ↑f.symm ⁻¹' s
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
⊢ I.target = ↑I '' I.source

Tactic:
exact I.image_source_eq_target.symm

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
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I y ∈ interior (f.extend I).target

Tactic:
rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq,
    mem_inter_iff, mem_preimage]
  exact ⟨mem_of_eq_of_mem (I.left_inv (y)) hy, hy'⟩

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
h : IsRCLikeNormedField 𝕜
⊢ UniqueDiffOn 𝕜 (range ↑I)

pp: case neg
𝕜 : 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
h : ¬IsRCLikeNormedField 𝕜
⊢ UniqueDiffOn 𝕜 (range ↑I)

Tactic:
· let := h.rclike 𝕜
    let := NormedSpace.restrictScalars ℝ 𝕜 E
    apply uniqueDiffOn_convex_of_isRCLikeNormedField _ I.nonempty_interior
    simpa [h] using I.convex_range

Goal state after:
case neg
𝕜 : 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
h : ¬IsRCLikeNormedField 𝕜
⊢ UniqueDiffOn 𝕜 (range ↑I)
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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ (g ∘ ↑(f.extend I).symm) (↑(f.extend I) z) ∈ f'.source

Tactic:
rw [comp_apply, extend_left_inv _ hz.2]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
s : Set M
f' : OpenPartialHomeomorph M' H'
g : M → M'
y : M
hy : y ∈ f.source
hgy : g y ∈ f'.source
hmaps : MapsTo g s f'.source
z : M
hz : z ∈ s ∩ f.source
⊢ g z ∈ 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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (e.extend I).symm.source ∩ ↑(e.extend I).symm ⁻¹' (e'.extend I).source = ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I

Tactic:
e'.extend_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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (e.extend I).symm.source ∩ ↑(e.extend I).symm ⁻¹' e'.source = ↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I
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
e e' : OpenPartialHomeomorph M H
x : E
hx : x ∈ (extendCoordChange e e').source
⊢ (extendCoordChange e e').source ∈ 𝓝[range ↑I] x

Tactic:
rw [I.extendCoordChange_source] at hx ⊢

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
e e' : OpenPartialHomeomorph M H
x : E
hx : x ∈ ↑I '' (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] 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
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
x : E
hx : x ∈ (extendCoordChange e e').source
⊢ (extendCoordChange e e').source ∈ 𝓝[range ↑I] x

Tactic:
rw [I.extendCoordChange_source] at hx ⊢

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
x : E
hx : x ∈ ↑I '' (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ (interior (range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv))).Nonempty

Tactic:
by
    rw [PartialEquiv.pi_apply, Set.range_piMap]
    simp [interior_pi_set finite_univ, univ_pi_nonempty_iff, nonempty_interior]

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

Goal state before:
pp: m 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✝
M : Type u_4
inst✝ : TopologicalSpace M
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy1 : y ∈ ↑I.symm ⁻¹' u
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
⊢ ∃ u_1,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      y ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)

Tactic:
← hx

Goal state after:
m 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✝
M : Type u_4
inst✝ : TopologicalSpace M
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hy1 : ↑I x ∈ ↑I.symm ⁻¹' u
hx : ↑I x = y
⊢ ∃ u_1,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      ↑I x ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m 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
M : Type u_4
inst✝ : TopologicalSpace M
f g : H → H
u : Set H
x✝ : IsOpen[inst✝¹] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
y : E
hy1 : y ∈ ↑I.symm ⁻¹' u
hy2 : y ∈ range ↑I
x : H
hx : ↑I x = y
⊢ (↑I ∘ g ∘ ↑I.symm) y = (↑I ∘ f ∘ ↑I.symm) y

Tactic:
← hx

Goal state after:
m 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
M : Type u_4
inst✝ : TopologicalSpace M
f g : H → H
u : Set H
x✝ : IsOpen[inst✝¹] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H
hy1 : ↑I x ∈ ↑I.symm ⁻¹' u
hx : ↑I x = y
⊢ (↑I ∘ g ∘ ↑I.symm) (↑I x) = (↑I ∘ f ∘ ↑I.symm) (↑I x)