mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
hn : n ≠ 0
⊢ IsClosed[inst✝²] (ModelWithCorners.boundary M)

Tactic:
← I.compl_interior,

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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
hn : n ≠ 0
⊢ IsClosed[inst✝²] (ModelWithCorners.interior M)ᶜ
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ =
    (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ

Tactic:
compl_prod_eq_union

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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ =
    (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝⁷] a
ha' : a ⊆ e.baseSet
h : MDiff[a] (T% s)
x : B
hx : x ∈ a
⊢ (MDiffAt[a] fun x ↦ (↑e ⟨x, s x⟩).2) x

Tactic:
have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝⁷] a
ha' : a ⊆ e.baseSet
h : MDiff[a] (T% s)
x : B
hx : x ∈ a
this : MDiffAt (T% s) x
⊢ (MDiffAt[a] fun x ↦ (↑e ⟨x, s x⟩).2) x
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝⁷] a
ha' : a ⊆ e.baseSet
h : MDiff[a] fun x ↦ (↑e ⟨x, s x⟩).2
x : B
hx : x ∈ a
⊢ MDiffAt[a] (T% s) x

Tactic:
have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx

Goal state after:
case refine_2
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝⁷] a
ha' : a ⊆ e.baseSet
h : MDiff[a] fun x ↦ (↑e ⟨x, s x⟩).2
x : B
hx : x ∈ a
this : (MDiffAt fun x ↦ (↑e ⟨x, s x⟩).2) x
⊢ MDiffAt[a] (T% s) x
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst✝¹³] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ MDiff fun x ↦ ⟨x, (ψ • s) x⟩

Tactic:
apply mdifferentiable_of_mdifferentiableOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
      (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
  · apply ((mdifferentiable_zeroSection _ _).mdifferentiableOn (s := (tsupport ψ)ᶜ)).congr
    intro y hy
    simp [image_eq_zero_of_notMem_tsupport hy, zeroSection]
  · exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'

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

Goal state before:
pp: case e'_5
𝕜 : 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✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun g ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I fun p ↦ p.1 * p.2
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ContMDiff.comp (ContMDiff.comp S₃ S₂) S₁
g : G
e_4✝ : g = (((F₃ ∘ F₂) ∘ F₁) g).proj
⊢ mulInvariantVectorField v g =
    ((mfderiv% fun z ↦
            (z, ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.2).1 *
              (z, ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.2).2)
          ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.1)
        ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).snd.1 +
      ((mfderiv% fun z ↦
            (((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.1, z).1 *
              (((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.1, z).2)
          ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.2)
        ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).snd.2

Tactic:
simp +instances [mulInvariantVectorField]

Goal state after:
Module: Mathlib.Topology.Homeomorph.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ Continuous e.invFun

Tactic:
simp only [Equiv.invFun_as_coe]

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ Continuous ⇑e.symm
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦ toLp 2 fun x_1 ↦ w - x

Tactic:
apply contDiff_euclidean.2 (fun i ↦ by fun_prop)

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦ toLp 2 fun x ↦ y - w

Tactic:
apply contDiff_euclidean.2 (fun i ↦ by fun_prop)

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↑w
A : ContMDiffAt (𝓡∂ 1) 𝓘(ℝ, ℝ) n (fun z ↦ ↑z) w
⊢ ContMDiffAt (𝓡∂ 1) I n f w

Tactic:
← contMDiffWithinAt_univ

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hf : ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↑w
A : ContMDiffWithinAt (𝓡∂ 1) 𝓘(ℝ, ℝ) n (fun z ↦ ↑z) univ w
⊢ ContMDiffWithinAt (𝓡∂ 1) I n f univ w
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
⊢ ↑x = a • v + ↑y

Tactic:
← ((ℝ ∙ v).starProjection_add_starProjection_orthogonal x),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
⊢ (ℝ ∙ v).starProjection ↑x + (ℝ ∙ v)ᗮ.starProjection ↑x = a • v + ↑y
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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 : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffAt (J.prod I) I' n (uncurry f) (x₀, g x₀)
hg : ContMDiffAt J I m g x₀
hmn : m + 1 ≤ n
⊢ ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀)
    x₀

Tactic:
← contMDiffWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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 : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiff[s]
⊢ ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)

Tactic:
intro x₀ hx₀

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiff[s]
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case e'_13
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := ⋯
e_3✝ : ↥(ℝ ∙ ↑(-v))ᗮ = ↥(ℝ ∙ -↑v)ᗮ
⊢ U.symm 0 = 0

Tactic:
set_option backward.isDefEq.respectTransparency false in
    simp

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Goal state before:
pp: EB : Type u_1
inst✝¹³ : NormedAddCommGroup EB
inst✝¹² : NormedSpace ℝ EB
HB : Type u_2
inst✝¹¹ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst✝¹⁰ : TopologicalSpace B
inst✝⁹ : ChartedSpace HB B
F : Type u_4
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : B → Type u_5
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : (x : B) → NormedAddCommGroup (E x)
inst✝⁴ : (x : B) → InnerProductSpace ℝ (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle ℝ F E
F₁ : Type u_6
inst✝¹ : NormedAddCommGroup F₁
inst✝ : InnerProductSpace ℝ F₁
⊢ IsContMDiffRiemannianBundle IB n F₁ (Trivial B F₁)

Tactic:
refine ⟨fun x ↦ innerSL ℝ, fun x ↦ ?_, fun x v w ↦ rfl⟩
  simp only [contMDiffAt_section]
  convert! contMDiffAt_const (c := innerSL ℝ)
  ext v w
  simp [hom_trivializationAt_apply, inCoordinates]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
F : Type u_5
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝²³ : TopologicalSpace (TotalSpace F V)
inst✝²² : (x : M) → AddCommGroup (V x)
inst✝²¹ : (x : M) → Module 𝕜 (V x)
inst✝²⁰ : (x : M) → TopologicalSpace (V x)
inst✝¹⁹ : FiberBundle F V
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
inst✝¹⁶ : TopologicalSpace (TotalSpace F' V')
inst✝¹⁵ : (x : M) → AddCommGroup (V' x)
inst✝¹⁴ : (x : M) → Module 𝕜 (V' x)
inst✝¹³ : (x : M) → TopologicalSpace (V' x)
inst✝¹² : FiberBundle F' V'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x
this✝⁶ : T2Space (V x)
this✝⁵ : FiniteDimensional 𝕜 (V x)
this✝⁴ : T2Space (V' x)
this✝³ : FiniteDimensional 𝕜 (V' x)
this✝² : IsTopologicalAddGroup (V x)
this✝¹ : IsTopologicalAddGroup (V' x)
this✝ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V' x)
v₁ v₂ : V x
w : V' x
⊢ (MDiffAt fun x_1 ↦ ⟨x_1, (extend F v₁ + extend F v₂) x_1⟩) x

Tactic:
exact mdifferentiableAt_add_section (mdifferentiableAt_extend ..)
          (mdifferentiableAt_extend ..)

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)

Tactic:
apply Nat.card_le_card_of_surjective (f := ConjClasses.map (QuotientGroup.mk' H))
    exact ConjClasses.map_surjective Quotient.mk''_surjective

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
rw [h0, reciprocalFactors_zero, commProb_cons, commProb_nil, mul_one, Nat.cast_zero, div_zero]
    apply commProb_eq_zero_of_infinite

Goal state after:
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
⊢ (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inr 1)) = 1

Tactic:
by simp only [MonoidHom.comp_apply, map_of, Sum.swap_inr, mk_of_inl, map_one]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
x : CoprodI M
hx : x ∈ ⋃ i, range ⇑of
y : CoprodI M
ihy : motive y
⊢ ∃ i m, of m = x

Tactic:
by simpa using hx

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B✝ : Type u_1
inst✝⁷ : TopologicalSpace B✝
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B✝ → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B✝) → NormedAddCommGroup (E x)
inst✝² : (x : B✝) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B✝
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
⊢ ∃ δ, 0 < δ ∧ 1 + δ * C < r' ^ 2

Tactic:
have B' : ∀ᶠ δ in 𝓝[>] 0, 1 + δ * C < r' ^ 2 := by
      apply (tendsto_order.1 B).2
      simpa using hr'.trans_le (le_abs_self _)

Goal state after:
B✝ : Type u_1
inst✝⁷ : TopologicalSpace B✝
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B✝ → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B✝) → NormedAddCommGroup (E x)
inst✝² : (x : B✝) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B✝
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C))
B' : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 1 + δ * C < r' ^ 2
⊢ ∃ δ, 0 < δ ∧ 1 + δ * C < r' ^ 2
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
⊢ rcons p = of p.head • p.tail

Tactic:
simp [of_smul_def]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝ : AddCommGroup M
x : DivisibleHull M
⊢ 0 • x = 0

Tactic:
simp [qsmul_def]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ (cs.leftInvSeq (alternatingWord i j (2 * p)))[k + 1] = cs.wordProd (alternatingWord j i (2 * (k + 1) + 1))

Tactic:
| succ k hk =>

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k < 2 * p
⊢ (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))

Tactic:
by
  induction k generalizing i j with
  | zero =>
    simp only [CoxeterSystem.getElem_leftInvSeq cs (alternatingWord i j (2 * p)) 0 (by simp [h]),
      take_zero, wordProd_nil, one_mul, inv_one, mul_one, alternatingWord, concat_eq_append,
      nil_append, wordProd_singleton]
    simp only [getElem_alternatingWord i j (2 * p) 0 (by simp [h]), add_zero, even_two,
      Even.mul_right, ↓reduceIte]
  | succ k hk =>
    simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by lia),
      MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
      ↓reduceIte, wordProd_cons]
    rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
    simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
⊢ a • 0 = 0

Tactic:
simp [qsmul_def]

Goal state after: