mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case hf.hg
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 := ⋯
g' : ℝ → F := ⋯
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
t : ℝ
ht : t ∈ Icc 0 1
⊢ HasDerivWithinAt (fun t ↦ (t * h ^ 2) • (f'' v) w) (h ^ 2 • (f'' v) w) (Icc 0 1) t

Tactic:
apply_rules [HasDerivAt.hasDerivWithinAt, HasDerivAt.smul_const, hasDerivAt_mul_const]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
⊢ HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v

Tactic:
apply hasDerivWithinAt_congr_set

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
⊢ (fun t ↦ x + t • v) ⁻¹' s =ᶠ[𝓝 0] (fun t ↦ x + t • v) ⁻¹' t
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
⊢ lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v

Tactic:
by
  apply derivWithin_congr_set
  let F := fun (t : 𝕜) ↦ x + t • v
  have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
  have : s =ᶠ[𝓝 (F 0)] t := by convert! h; simp [F]
  exact B.preimage_mem_nhds this

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

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

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:
· simp only [zero_smul, _root_.sign_zero, SignType.coe_zero]
        exact fderiv_zero_of_not_differentiableAt <| not_differentiableAt_norm_zero E

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
⊢ fderiv ℝ (fun x ↦ ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x ↦ ‖x‖) x
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
x : E
inst✝ : Nontrivial E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
this : x ≠ 0
⊢ 1 * ‖x‖ = (fderiv ℝ (fun x ↦ ‖x‖) x) x

Tactic:
rw [one_mul, h.fderiv_norm_self]

Goal state after:
Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u, f v = f u ↔ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2

Tactic:
let φ := dfu.implicitFunctionDataOfProdDomain if₂u

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := dfu.implicitFunctionDataOfProdDomain if₂u
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u, f v = f u ↔ dfu.implicitFunctionOfProdDomain if₂u v.1 = v.2
Module: Mathlib.Analysis.Calculus.LagrangeMultipliers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
H₁ : Λ (f' x) = f' x * Λ 1
H₂ : f' x * Λ 1 + Λ₀ * φ' x = 0
⊢ (Λ 1 • f' + Λ₀ • φ') x = 0 x

Tactic:
simpa [mul_comm] using H₂

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
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|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ ∃ ε, μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1) ∧ 0 < ε

Tactic:
have L1 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (μ (A '' closedBall 0 1))) := by
      apply L0.congr' _
      filter_upwards [self_mem_nhdsWithin] with r hr
      rw [← HC.add_closedBall_zero (le_of_lt hr), add_comm]

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|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ ∃ ε, μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1) ∧ 0 < ε
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inl
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
hm : ↑0 < ENNReal.ofReal |A.det|
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑0 * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0

Tactic:
filter_upwards

Goal state after:
case inl
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
hm : ↑0 < ENNReal.ofReal |A.det|
⊢ ∀ (a : ℝ≥0) (s : Set E) (f : E → E), ApproximatesLinearOn f A s a → ↑0 * μ s ≤ μ (f '' s)
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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
fint : IntegrableOn f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
⊢ Tendsto f atBot (𝓝 0)

Tactic:
have Fderiv : ∀ x ∈ Iic a, HasDerivAt (F ∘ f) (F (f' x)) x :=
    fun x hx ↦ F.hasFDerivAt.comp_hasDerivAt _ (hderiv x hx)

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

Goal state before:
pp: case pos.inr.hfg'
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
v : E
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)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := ⋯
E' : Type := ⋯
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := ⋯
L_emb : MeasurableEmbedding ⇑L
⊢ Integrable (fun x ↦ (B (f (L.symm x))) (g' (L.symm x))) ν

Tactic:
simpa [ν, L_emb.integrable_map_iff, Function.comp_def] using hfg'

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
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n))

Tactic:
rw [← image_iUnion, ← inter_iUnion]
      gcongr
      exact subset_inter Subset.rfl t_cover

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ TendstoLocallyUniformlyOn (fun N b ↦ ∏ i ∈ Finset.range N, f i b) g atTop s

Tactic:
intro v hv r hr

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
s : Set β
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
hv : v ∈ uniformity α
r : β
hr : r ∈ s
⊢ ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun N b ↦ ∏ i ∈ Finset.range N, f i b) n y) ∈ v
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)
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε

Tactic:
rintro ε hε

Goal state after:
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) < ε
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

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

Tactic:
by
  rcases φ.eq_or_neBot with rfl | hne
  · simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
  have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn.frequently
  rw [tendstoUniformlyOn_iff] at hF ⊢
  rintro ε hε
  filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz
  simp_rw [dist_eq_norm] at h ⊢
  have e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ := fun w hw1 =>
    h w (closedBall_subset_cthickening hz δ (sphere_subset_closedBall hw1))
  have e3 := sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ)
  have hf : ContinuousOn f (sphere z δ) :=
    e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))
  simpa only [mul_div_cancel_right₀ _ hδ.ne.symm] using! norm_cderiv_sub_lt hδ e2 hf (h'.mono e3)

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

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U

Tactic:
tendstoLocallyUniformlyOn_iff_forall_isCompact hU

Goal state after:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case refine_1
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
⊢ x ∈ e.source → ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members

Tactic:
hex

Goal state after:
case refine_1
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case refine_2
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
⊢ x ∈ e.source → ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G'.members

Tactic:
hex

Goal state after:
case refine_2
H : Type u_1
inst✝ : TopologicalSpace H
G G' : StructureGroupoid H
e : OpenPartialHomeomorph H H
hx : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G.members ∩ G'.members
x : H
hex : x ∈ e.source
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ G'.members
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ ∀ i ∈ S, e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
x : H
⊢ x ∈ e.source → ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ i.members

Tactic:
hex

Goal state after:
H : Type u_1
inst✝ : TopologicalSpace H
S : Set (StructureGroupoid H)
e : OpenPartialHomeomorph H H
he : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ ∀ i ∈ S, e.restr s ∈ i.members
i : StructureGroupoid H
hi : i ∈ S
x : H
hex : x ∈ e.source
⊢ ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ i.members
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
hc : c ∈ atlas H M'
hc' : c' ∈ atlas H M
this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c'.symm.symm ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G

Tactic:
symm_symm,

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'
hc' : c' ∈ atlas H M
this : (c.symm ≫ₕ e.toOpenPartialHomeomorph.symm) ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ e.symm.toOpenPartialHomeomorph ≫ₕ c' ∈ G
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_1
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 : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' ↑e.symm ⁻¹' s) x
x' : H
hx' : x' ∈ e.source
⊢ f (↑e.symm (↑e x')) = f x'

Tactic:
e.left_inv hx'

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

Goal state before:
pp: case refine_2
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 : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' ↑e.symm ⁻¹' s) x
x' : H
hx' : x' ∈ e.source
⊢ ↑e.symm (↑e x') ∈ s ↔ x' ∈ s

Tactic:
e.left_inv hx'

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
hs : s ⊆ f.source
⊢ map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I) '' s] ↑(f.extend I) y

Tactic:
by
  rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]
  rwa [extend_source]

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

Goal state before:
pp: H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : OpenPartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
· exact hgs.comp (e.symm.continuousAt <| e.mapsTo xe).continuousWithinAt Subset.rfl

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ s ⊆ univ

Tactic:
exact subset_univ _

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

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

Tactic:
have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)

Goal state after:
case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
this : ContinuousWithinAt ((f ∘ ↑I.symm) ∘ ↑I) (↑I ⁻¹' (↑I.symm ⁻¹' s ∩ range ↑I)) x
⊢ ContinuousWithinAt f s x
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 v : Set H
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
hg : ContDiffOn 𝕜 n (↑I ∘ g ∘ ↑I.symm) (↑I.symm ⁻¹' v ∩ range ↑I)
x✝² : IsOpen[inst✝¹] u
x✝¹ : IsOpen[inst✝¹] v
x✝ : IsOpen[inst✝¹] (u ∩ f ⁻¹' v)
this : ↑I ∘ (g ∘ f) ∘ ↑I.symm = (↑I ∘ g ∘ ↑I.symm) ∘ ↑I ∘ f ∘ ↑I.symm
x : E
hx1 : x ∈ ↑I.symm ⁻¹' (u ∩ f ⁻¹' v)
right✝ : x ∈ range ↑I
⊢ (↑I ∘ f ∘ ↑I.symm) x ∈ ↑I.symm ⁻¹' v ∩ range ↑I

Tactic:
simp only [mfld_simps] at hx1 ⊢

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 v : Set H
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
hg : ContDiffOn 𝕜 n (↑I ∘ g ∘ ↑I.symm) (↑I.symm ⁻¹' v ∩ range ↑I)
x✝² : IsOpen[inst✝¹] u
x✝¹ : IsOpen[inst✝¹] v
x✝ : IsOpen[inst✝¹] (u ∩ f ⁻¹' v)
this : ↑I ∘ (g ∘ f) ∘ ↑I.symm = (↑I ∘ g ∘ ↑I.symm) ∘ ↑I ∘ f ∘ ↑I.symm
x : E
right✝ : x ∈ range ↑I
hx1 : ↑I.symm x ∈ u ∧ f (↑I.symm x) ∈ v
⊢ f (↑I.symm x) ∈ v
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
⊢ (interior (extChartAt I x).target).Nonempty

Tactic:
by
  by_contra! H
  have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)
  simp only [H, closure_empty, mem_empty_iff_false] at this

Goal state after: