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

Goal state before:
pp: case refine_4
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ (hf.domChart.restr s).source ⊆ g ⁻¹' hf.codChart.source

Tactic:
trans s' ∩ f ⁻¹' hf.codChart.source

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ (hf.domChart.restr s).source ⊆ s' ∩ f ⁻¹' hf.codChart.source

𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ s' ∩ f ⁻¹' hf.codChart.source ⊆ g ⁻¹' hf.codChart.source
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case e_a
𝕜 : 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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
f' : E → 𝕜 := f ∘ ↑(extChartAt I x).symm
s' : Set E := ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ (fderivWithin 𝕜 f' s' x₀) (V' x₀) • W' x₀
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) A x = (d[s] f x) (V x) • W x

Tactic:
simpa only [A] using! mpullback_mfderivWithin_apply_smul hf

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
⊢ IsImmersionAtOfComplement PUnit.{u_15 + 1} I I n id x

Tactic:
apply IsImmersionAtOfComplement.mk_of_continuousAt (continuousAt_id) (.prodUnique 𝕜 E _)
    (chartAt H x) (chartAt H x) (mem_chart_source H x) (mem_chart_source H x)
    (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x)

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
⊢ EqOn (↑((chartAt H x).extend I) ∘ id ∘ ↑((chartAt H x).extend I).symm)
    (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}) ∘ fun x ↦ (x, 0)) ((chartAt H x).extend I).target
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ (mfderiv[Icc x y] (projIcc x y ⋯) z) 1 = oneTangentSpaceIcc (projIcc x y ⋯ z)

Tactic:
simp only [oneTangentSpaceIcc]

Goal state after:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ (mfderiv[Icc x y] (projIcc x y ⋯) z) 1 = (mfderiv[Icc x y] (projIcc x y ⋯) ↑(projIcc x y ⋯ z)) 1
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersionOfComplement F J J' n φ
⊢ ContMDiff I J n f ↔ Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)

Tactic:
refine ⟨fun h ↦ ⟨h.continuous, hφ.contMDiff.comp h⟩, fun ⟨h, h'⟩ x ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersionOfComplement F J J' n φ
x✝ : Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)
x : M
h : Continuous[inst✝⁵, inst✝³] f
h' : ContMDiff I J' n (φ ∘ f)
⊢ ContMDiffAt I J n f x
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
w : E
hw : w ∈ (ℝ ∙ v)ᗮ
h₁ : 0 < ‖w‖ ^ 2 + 4
this : ‖4 • w + (‖w‖ ^ 2 - 4) • v‖ = ‖w‖ ^ 2 + 4
⊢ stereoInvFunAux v w ∈ sphere 0 1

Tactic:
by
    simp only [mem_sphere_zero_iff_norm, norm_smul, Real.norm_eq_abs, abs_inv, this,
      abs_of_pos h₁, stereoInvFunAux_apply, inv_mul_cancel₀ h₁.ne']

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I ×ˢ range ↑I') (↑I w, ↑I' w')

Tactic:
apply UniqueDiffWithinAt.prod

Goal state after:
case hs
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑I w)

case ht
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I') (↑I' w')
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y

Tactic:
rcases exists_between hab with ⟨a', haa', ha'b⟩

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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y
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
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun m ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) 1 fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
⊢ MDiffAt[s] b x

Tactic:
simp only [mdifferentiableWithinAt_totalSpace] at hv

Goal state after:
EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) 1 fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
hv : (MDiffAt[s] fun x ↦ b x) x ∧ (MDiffAt[s] fun x_1 ↦ (↑(trivializationAt F E (b x)) ⟨b x_1, v x_1⟩).2) x
⊢ MDiffAt[s] b x
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

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
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ IsVonNBounded ℝ {v | ((innerSL ℝ) v) v < 1}

Tactic:
change IsVonNBounded ℝ {v : F | ⟪v, v⟫ < 1}

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiff[s]
hu : UniqueMDiff[u]
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst✝⁹] (interior u)
hsu : s ⊆ u
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

Tactic:
by
  have B : ContDiffWithinAt 𝕜 n ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
      ((extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (extChartAt I x₀ x₀) := by
    apply (contMDiffWithinAt_iff.1 hf).2.congr_set
    exact EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq.symm
  apply mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt hV hW hs
    ((hf.mono hsu).of_le (le_minSmoothness.trans hn)) hx₀ hst
  have : ((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target : Set E)
      =ᶠ[𝓝 (extChartAt I x₀ x₀)] ((extChartAt I x₀).symm ⁻¹' s ∩ range I : Set E) :=
    EventuallyEq.inter (by rfl) extChartAt_target_eventuallyEq
  apply IsSymmSndFDerivWithinAt.congr_set _ this
  have : IsSymmSndFDerivWithinAt 𝕜 ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
      ((extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (extChartAt I x₀ x₀) := by
    apply ContDiffWithinAt.isSymmSndFDerivWithinAt (n := minSmoothness 𝕜 2) _ le_rfl
    · rw [inter_comm]
      exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀
    · apply extChartAt_mem_closure_interior h'x₀ (mem_extChartAt_source x₀)
    · simp [hsu hx₀]
    · exact B.of_le hn
  apply IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin this
  · apply mem_of_superset self_mem_nhdsWithin (inter_subset_inter_left _ (preimage_mono hsu))
  · exact (B.of_le hn).of_le le_minSmoothness
  · rw [inter_comm]
    exact UniqueMDiffOn.uniqueDiffOn_target_inter hs x₀
  · rw [inter_comm]
    exact UniqueMDiffOn.uniqueDiffOn_target_inter hu x₀
  · simp [hx₀]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card (M × M')) ^ 2 =
    ↑(Nat.card { p // Commute p.1 p.2 }) * ↑(Nat.card { p // Commute p.1 p.2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
Nat.card_prod,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M * Nat.card M') ^ 2 =
    ↑(Nat.card { p // Commute p.1 p.2 }) * ↑(Nat.card { p // Commute p.1 p.2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card (ZMod n) + (Nat.card (ZMod n) + (Nat.card (ZMod n) + Nat.card (ZMod n × ZMod n))) = n * (n + 3)

Tactic:
Nat.card_prod,

Goal state after:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card (ZMod n) + (Nat.card (ZMod n) + (Nat.card (ZMod n) + Nat.card (ZMod n) * Nat.card (ZMod n))) = n * (n + 3)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) =
    Nat.card (ConjClasses (DihedralGroup n)) * Nat.card (DihedralGroup n) / (2 * n)

Tactic:
nat_card,

Goal state after:
n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = Nat.card (ConjClasses (DihedralGroup n)) * (2 * n) / (2 * n)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) ≠ cs.length w

Tactic:
rw [← length_inv]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w)⁻¹ ≠ cs.length w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ Function.RightInverse (fun w ↦ w.prod) fun m ↦ m • empty

Tactic:
by
    apply smul_induction
    · dsimp only
      rw [prod_empty, one_smul]
    · dsimp only
      intro i m w ih
      rw [prod_smul, mul_smul, ih]

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
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * t * t'

Tactic:
rw [mul_assoc, h₄]; group

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i : ι
w : NeWord H i i
⊢ (lift f) w.prod ≠ 1

Tactic:
obtain ⟨k, hk⟩ := exists_ne i
  exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hk hk

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s < mk m' s' ↔ ↑s' • m < ↑s • m'

Tactic:
by
  simp_rw [lt_iff_not_ge, mk_le_mk]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : DecidableEq G
R S : Finset G
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ↑(Finset.image (fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_mul]
  exact closure_mul_image_eq_top hR hR1 hS

Goal state after:
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
⊢ Commute g h

Tactic:
by
  have key := map_mul φ g h
  rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : ↥H
⊢ ⁅a, b⁆ ∈ {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}

Tactic:
exact ⟨a, a.2, b, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ ∏ q,
      (QuotientGroup.mk' H.focalSubgroupOf)
        ⟨(Quotient.out q.out)⁻¹ * ↑x ^ minimalPeriod (fun x_1 ↦ ↑x • x_1) q.out * Quotient.out q.out, ⋯⟩ =
    ∏ i, ↑x ^ minimalPeriod (fun x_1 ↦ ↑x • x_1) i.out

Tactic:
apply Finset.prod_congr rfl

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ ∀ x_1 ∈ Finset.univ,
    (QuotientGroup.mk' H.focalSubgroupOf)
        ⟨(Quotient.out x_1.out)⁻¹ * ↑x ^ minimalPeriod (fun x_2 ↦ ↑x • x_2) x_1.out * Quotient.out x_1.out, ⋯⟩ =
      ↑x ^ minimalPeriod (fun x_2 ↦ ↑x • x_2) x_1.out
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
a b : G
ha : a ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
hb : b ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅a * b, y⁆ ∈ N

Tactic:
convert! Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y) using 1

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
a b : G
ha : a ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
hb : b ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅a * b, y⁆ = ⁅a, b * y * b⁻¹⁆ * ⁅b, y⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
intro n hn
    exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a ≤ b
hn : upperCentralSeries G a = upperCentralSeries G (a + 1)
⊢ upperCentralSeries G a = upperCentralSeries G b

Tactic:
refine Nat.le_induction rfl ?_ b ab

Goal state after:
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a ≤ b
hn : upperCentralSeries G a = upperCentralSeries G (a + 1)
⊢ ∀ (n : ℕ),
    a ≤ n → upperCentralSeries G a = upperCentralSeries G n → upperCentralSeries G a = upperCentralSeries G (n + 1)