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

Goal state before:
pp: case hττ'
𝕜 : 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 x
w₁ w₂ : V' x
⊢ extend F' (w₁ + w₂) x = (extend F' w₁ + extend F' w₂) x

Tactic:
simp

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

Goal state before:
pp: case hττ'
𝕜 : 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)
c : 𝕜
v : V x
w : V' x
⊢ extend F' (c • w) x = ((fun x ↦ c) • extend F' w) x

Tactic:
simp

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
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
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
τ : (x : M) → V' x
hτ : MDiffAt (T% τ) x
⊢ extend F (σ x) x = σ x

Tactic:
simp

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
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
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
τ : (x : M) → V' x
hτ : MDiffAt (T% τ) x
⊢ extend F' (τ x) x = τ x

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
hx's : x' ∉ s
⊢ 0 • σ x' = 0 • σ' x'

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
hf

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
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + 1 x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + 1 x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mpr
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
x : M
u v : TangentSpace I x
⊢ mlieBracket I (extend E u) (extend E v) x - mlieBracket I (extend E u) (extend E v) x = ((0 x) u) v

Tactic:
simp

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
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ δ * ‖w‖ ^ 2 + ((g' y) w) w ≤ δ * ‖↑G (G.symm w)‖ ^ 2 + ((g' y) w) w

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ poly.vertices 0 = poly.vertices ((finRotate 1) 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : Nontrivial R
inst✝ : NeZero 2
poly : Polygon P 2
h : HasNondegenerateVertices R poly
this : 2 ≤ 2
hlt : 2 < 3
⊢ ![poly.vertices 0, poly.vertices (0 + 1), poly.vertices (0 + 2)] 0 =
    ![poly.vertices 0, poly.vertices (0 + 1), poly.vertices (0 + 2)] 2

Tactic:
simp

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

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E := ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)
⊢ ∞ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_5
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) = Nat.card ↥(Subgroup.center G)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ i, (↑i).carrier.toFinset.card = ∑ i, Nat.card ↑(↑i).carrier

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ i_1 ∈ Set.univ, map (MonoidHom.mulSingle Gs i) (H i) ≤ comap (Pi.evalMonoidHom Gs i_1) (H i_1)

Tactic:
intro j

Goal state after:
case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
⊢ j ∈ Set.univ → map (MonoidHom.mulSingle Gs i) (H i) ≤ comap (Pi.evalMonoidHom Gs j) (H j)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ i_1 ∈ Set.univ, map (MonoidHom.mulSingle Gs i) (K i) ≤ comap (Pi.evalMonoidHom Gs i_1) (K i_1)

Tactic:
intro j

Goal state after:
case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
⊢ j ∈ Set.univ → map (MonoidHom.mulSingle Gs i) (K i) ≤ comap (Pi.evalMonoidHom Gs j) (K j)
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.mpr inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.mp inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq ⋯
x : M
⊢ ∞ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Mul α
inst✝ : Infinite α
a₁✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ ⟨(a, a), ⋯⟩) a₁✝ = (fun a ↦ ⟨(a, a), ⋯⟩) a₂ → a₁✝ = a₂

Tactic:
simp

Goal state after:
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
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
x : M
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) univ x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) univ x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) univ x
⊢ x ∈ closure[inst✝³] (interior univ)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: ⊢ Nat.card (ZMod 2 × ZMod 2) = 4

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ AddMonoid.exponent (Additive G) = 2

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Monoid.exponent (Multiplicative G) = 2

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x : G
⊢ Monoid.exponent G = 2

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ Monoid.exponent G = 2

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Fintype.card G₁ = Fintype.card G₂

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
_inst₁✝ : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ ((Fintype.equivOfCardEq ⋯).setValue 1 1) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
⊢ r 1 ^ n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
i : ZMod n
⊢ sr i * sr i = 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card ↥H) ^ 2 ≤
    ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card G) ^ 2 * ↑H.index ^ 2

Tactic:
div_le_iff₀,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) ≤
    ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card G) ^ 2 * ↑H.index ^ 2 * ↑(Nat.card ↥H) ^ 2

G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2
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 (G ⧸ H)) ≤ ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G) * ↑(Nat.card ↥H)

Tactic:
div_le_iff₀,

Goal state after:
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)) / ↑(Nat.card G) * ↑(Nat.card ↥H) * ↑(Nat.card (G ⧸ H))

G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝ : Group G
b : FreeGroupBasis ι G
i : ι
⊢ b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : Group H
b : FreeGroupBasis ι G
f : FreeGroup ι →* H
a✝ : ι
⊢ ((fun f ↦ f.comp b.repr.symm.toMonoidHom) ((fun f ↦ f.comp b.repr.toMonoidHom) f)) (FreeGroup.of a✝) =
    f (FreeGroup.of a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : Group H
b : FreeGroupBasis ι G
f : G →* H
x✝ : G
⊢ ((fun f ↦ f.comp b.repr.toMonoidHom) ((fun f ↦ f.comp b.repr.symm.toMonoidHom) f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: case one
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList 1)).reverse) * mk 1 = 1

Tactic:
simp

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

Goal state before:
pp: case h₁
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : M
⊢ (((Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e')).comp inl) x✝ = ((MonoidHom.id (M ∗ M')).comp inl) x✝

Tactic:
simp

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

Goal state before:
pp: case h₂
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : M'
⊢ (((Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e')).comp inr) x✝ = ((MonoidHom.id (M ∗ M')).comp inr) x✝

Tactic:
simp

Goal state after: