mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1) =
    (derivative p).roots.card + 1

Tactic:
rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
        Multiset.toFinset_sum_count_eq, ← Finset.sum_subset Finset.subset_union_right]
      intro x _ hx₂
      simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
a : (fun x ↦ x ^ p) '' Ioi 0 = Ioi 0
this : ∫ (x : ℝ) in Ioi 0, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y

Tactic:
this

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
a : (fun x ↦ x ^ p) '' Ioi 0 = Ioi 0
this : ∫ (x : ℝ) in Ioi 0, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

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

Tactic:
this

Goal state after:
case pos.inr.hf
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)) μ
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
hf : HasLineDerivAt ℝ ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) (f' (L.symm x)) (L.symm x) v
hx : x ∈ tsupport fun x ↦ g (L.symm x)
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
h2x : L.symm x ∈ tsupport g
⊢ HasLineDerivAt ℝ (fun x ↦ f (L.symm x)) (f' (L.symm x)) x (0, 1)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x ↦ x ^ p) S
a3 : (fun t ↦ t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Tactic:
this

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x ↦ x ^ p) S
a3 : (fun t ↦ t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔
    IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x ↦ x ^ p) S
a3 : (fun t ↦ t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ (|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x ↦ x ^ p) S
a3 : (fun t ↦ t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x ↦ |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ (|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: case hg
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
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
hg : HasLineDerivAt ℝ g (g' (L.symm x)) (L.symm x) v
hx : x ∈ tsupport fun x ↦ f (L.symm x)
this : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
h2x : L.symm x ∈ tsupport f
⊢ HasLineDerivAt ℝ (fun x ↦ g (L.symm x)) (g' (L.symm x)) x (0, 1)

Tactic:
this

Goal state after:
case hg
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
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (L.symm x)) (L.symm x) v
hx : x ∈ tsupport fun x ↦ f (L.symm x)
this : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
h2x : L.symm x ∈ tsupport f
⊢ HasLineDerivAt ℝ (fun x ↦ g (L.symm x)) (g' (L.symm x)) x (0, 1)
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w ↦ ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w ↦ ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
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 : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h : ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε * δ
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε

Tactic:
[

Goal state after:
E : Type u_1
ι : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h : ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε * δ
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
Module: Mathlib.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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
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) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ n, s ∩ t n
| μ.restrict s

Tactic:
this

Goal state after:
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := ⟨ε, ⋯⟩
δpos : 0 < δ
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) δ
right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun n ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ n, s ∩ t n
| μ.restrict (⋃ n, s ∩ t n)
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ e.symm ≫ₕ e ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_ e.symm_trans_self

Goal state after:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ ofSet e.target ⋯ ∈ G
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
⊢ ∀ (a : StructureGroupoid H), idGroupoid H ≤ a

Tactic:
by
    intro u f hf
    have hf :
        f ∈ {OpenPartialHomeomorph.refl H} ∪ { e : OpenPartialHomeomorph H H | e.source = ∅ } :=
      hf
    simp only [singleton_union, mem_ofPred_eq, mem_insert_iff] at hf
    rcases hf with hf | hf
    · rw [hf]
      apply u.id_mem
    · apply u.locality
      intro x hx
      rw [hf, mem_empty_iff_false] at hx
      exact hx.elim

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
s : Opens M
hs : Nonempty ↥s
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
e' : OpenPartialHomeomorph (↥s) H
he' : e' ∈ atlas H ↥s
x : ↥s
this : e' = (chartAt H ↑x).subtypeRestr hs
⊢ (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
this

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
s : Opens M
hs : Nonempty ↥s
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
e' : OpenPartialHomeomorph (↥s) H
he' : e' ∈ atlas H ↥s
x : ↥s
this : e' = (chartAt H ↑x).subtypeRestr hs
⊢ (e.subtypeRestr hs).symm ≫ₕ (chartAt H ↑x).subtypeRestr hs ∈ G ∧
    ((chartAt H ↑x).subtypeRestr hs).symm ≫ₕ e.subtypeRestr hs ∈ G
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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
n i : ℕ
⊢ MeasurableSet (spanningSets μ i)

Tactic:
exact measurableSet_spanningSets μ i

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
⊢ (f.extend I).target = ↑I.symm ⁻¹' f.target ∩ range ↑I

Tactic:
[

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
⊢ (f.extend I).target = ↑I.symm ⁻¹' f.target ∩ 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' f.target ∩ range ↑I)

Tactic:
I.range_eq_univ,

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
inst✝ : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' f.target ∩ univ)
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 : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
host : o ⊆ {x | x ∈ s ↔ x ∈ t}
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
⊢ P f s x ↔ P f t x

Tactic:
[

Goal state after:
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 : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
host : o ⊆ {x | x ∈ s ↔ x ∈ t}
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
⊢ P f s x ↔ P f t x
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 : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f s x ↔ P g s x

Tactic:
[

Goal state after:
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 g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f s x ↔ P g s 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
⊢ 𝓝[range ↑I] ↑(f.extend I) x = 𝓝 (↑(f.extend I) x)

Tactic:
I.range_eq_univ,

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
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
⊢ 𝓝[univ] ↑(f.extend I) x = 𝓝 (↑(f.extend I) x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case mpr
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'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f s x → P (↑e' ∘ f) s x

Tactic:
[

Goal state after:
case mpr
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'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f s x → P (↑e' ∘ f) s x
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:
[

Goal state after:
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'
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
⊢ x' ∈ ↑e ⁻¹' ↑e.symm ⁻¹' s ↔ x' ∈ s

Tactic:
[

Goal state after:
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
⊢ x' ∈ ↑e ⁻¹' ↑e.symm ⁻¹' s ↔ x' ∈ s
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

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

Tactic:
[

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'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ LiftProp P f ↔
    Continuous[inst✝⁴, inst✝¹] f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case hu.refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ↑e.symm (↑e x) ∈ (chartAt H x).source

Tactic:
[

Goal state after:
case hu.refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ↑e.symm (↑e x) ∈ (chartAt H x).source
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case hu.refine_2
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
y : H
hy : y ∈ ↑e.symm ⁻¹' (chartAt H x).source
⊢ y ∈ ↑((chartAt H x).symm ≫ₕ e).symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ↔ y ∈ ↑e.symm ⁻¹' s

Tactic:
[

Goal state after:
case hu.refine_2
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
y : H
hy : y ∈ ↑e.symm ⁻¹' (chartAt H x).source
⊢ y ∈ ↑((chartAt H x).symm ≫ₕ e).symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ↔ y ∈ ↑e.symm ⁻¹' s