mathlib-initiative/mathlib-tactics huggingface dataset:
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'δ : 1 + δ * C < r' ^ 2
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' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ δ * ‖w‖ ^ 2 + ((g' x) w) w ≤ δ * ‖↑G (G.symm w)‖ ^ 2 + ((g' x) w) w

Tactic:
]

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
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
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' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ δ * ‖w‖ ^ 2 + ((g' x) w) w ≤ δ * ‖↑G (G.symm w)‖ ^ 2 + ((g' x) w) w
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
⊢ ⊤.lowerCentralSeries n = ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
N : Subgroup G
inst✝⁴ : N.Normal
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsNilpotent G₁
inst✝ : IsNilpotent G₂
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: case e_5
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ f b✝ =
    f
      (have this := a✝;
      this)

Tactic:
]

Goal state after:
case e_5
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f
a✝ b✝ : Generators G
e✝ : a✝ ⟶ b✝
⊢ f b✝ =
    f
      (have this := a✝;
      this)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
ih : (pi Set.univ Ss).lowerCentralSeries n ≤ pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n
⊢ (pi Set.univ fun i ↦ ⁅(Ss i).lowerCentralSeries n, Ss i⁆) ≤ pi Set.univ fun i ↦ ⁅(Ss i).lowerCentralSeries n, Ss i⁆

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ (pi Set.univ fun i ↦ ⊤).lowerCentralSeries n ≤ pi Set.univ fun i ↦ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ (pi Set.univ fun i ↦ ⊤).lowerCentralSeries n ≤ pi Set.univ fun i ↦ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), ⊤.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ x ∈ Set.univ

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ x ∈ Set.univ
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
n : ℕ
⊢ (pi Set.univ fun i ↦ ⊤.lowerCentralSeries n) = pi Set.univ fun i ↦ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
]

Goal state after:
case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∀ (i : η), ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) = ⊥

Tactic:
]

Goal state after:
case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∀ (i : η), ⊤.lowerCentralSeries (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
i : η
⊢ nilpotencyClass (Gs i) ≤ Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)

Tactic:
]

Goal state after:
case intro
G : Type u_1
inst✝⁴ : Group G
N : Subgroup G
inst✝³ : N.Normal
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
val✝ : Fintype η
i : η
⊢ nilpotencyClass (Gs i) ≤ Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h : Group.IsNilpotent G
n : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ derivedSeries G n ≤ ⊤.lowerCentralSeries n

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h : Group.IsNilpotent G
n : ℕ
hn : ⊤.lowerCentralSeries n = ⊥
⊢ derivedSeries G n ≤ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer ↑H = H

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer ↑H = H
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ ⇑f '' univ = univ

Tactic:
]

Goal state after:
case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ ⇑f '' univ = univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
h : B = univ
⊢ univ = univ

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card (G ⧸ center G) * Nat.card ↥(center G)

Tactic:
]

Goal state after:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card (G ⧸ center G) * Nat.card ↥(center G)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ i ∈ s, Disjoint (g • B) (i • B)

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ ∀ i ∈ s, Disjoint (g • B) (i • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
⊢ g₂ • B₁ ∩ g₂ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ ⇑j ⁻¹' (φ g₂ • B)
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (⇑j ⁻¹' (φ g₂ • B))

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
hB : IsBlock G B
g₁ g₂ : H
hg : ⇑j ⁻¹' (φ g₁ • B) ≠ ⇑j ⁻¹' (φ g₂ • B)
⊢ Disjoint (⇑j ⁻¹' (φ g₁ • B)) (⇑j ⁻¹' (φ g₂ • B))
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ¬g₁ • B = g₂ • B → Disjoint (g₁ • B) (g₂ • B) ↔ g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
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'δ : 1 + δ * C < r' ^ 2
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' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ δ * (‖↑G‖ * ‖G.symm w‖) ^ 2 + ((g' x) w) w = δ * C * ‖G.symm w‖ ^ 2 + ((g' x) w) w

Tactic:
by ring

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = ↑h' • g • B

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = ↑h' • g • B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h) • B = (g * h) • B

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.map (↑(MulAut.conj g)) (Subgroup.comap ↑(MulAut.conj g) ⊤))) (g • B)

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.map (↑(MulAut.conj g)) (Subgroup.comap ↑(MulAut.conj g) ⊤))) (g • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) B

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • k • a = g • k • a

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) a)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ IsBlock G (orbit (↥N) a)

Tactic:
by
  rw [isBlock_iff_smul_eq_or_disjoint]
  intro g
  rw [smul_orbit_eq_orbit_smul]
  apply orbit.eq_or_disjoint

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • ↑s = b • ↑s

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • ↑s = b • ↑s

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ ⦃g : G⦄, (g • orbit (↥H) a ∩ orbit (↥H) a).Nonempty → g • orbit (↥H) a = orbit (↥H) a

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ ⦃g : G⦄, (g • orbit (↥H) a ∩ orbit (↥H) a).Nonempty → g • orbit (↥H) a = orbit (↥H) a
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a

Tactic:
]

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
this : g ∈ H
⊢ orbit (↥H) a = orbit (↥H) a

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a

Tactic:
Subgroup.smul_def,

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (↑g • a) ≤ N ⊔ IwaS.T a
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a

Tactic:
]

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ H