mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).domRestrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).domRestrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ (transferSylow P hP).ker.IsComplement' ↑P
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
key : g * h = h * g
⊢ Commute g h

Tactic:
]

Goal state after:
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
key : g * h = h * g
⊢ Commute g h
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 : G
hg : orderOf g = 2
⊢ 1 = 1

Tactic:
]

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 : G
hg : 1 = 2
key : φ g = g
⊢ False

Tactic:
]

Goal state after:
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 : G
hg : 1 = 2
key : φ g = g
⊢ False
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 ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
⊢ False

Tactic:
]

Goal state after:
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 ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
⊢ False
Module: Mathlib.GroupTheory.Focal

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑H
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (h k : G), h ∈ H.focalSubgroup → k ∈ H → k * h * k⁻¹ ∈ H.focalSubgroup

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (h k : G), h ∈ H.focalSubgroup → k ∈ H → k * h * k⁻¹ ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : (transferSylow P hP).ker ⊓ ↑P = ⊥ ∧ ↑(transferSylow P hP).ker * ↑↑P = Set.univ
this : Function.Surjective ⇑(transferSylow P hP)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
]

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : (transferSylow P hP).ker ⊓ ↑P = ⊥ ∧ ↑(transferSylow P hP).ker * ↑↑P = Set.univ
this : Function.Surjective ⇑(transferSylow P hP)
⊢ (transferSylow P hP).ker.IsComplement' ↑P
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑(_root_.commutator G)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} ⊆ ↑(_root_.commutator G)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ centralizer ↑P ≤ centralizer ↑P

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ↑(⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩) ∈ H.focalSubgroup

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ↑(⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩) ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
⊢ normalizer ↑P ≤ centralizer ↑P

Tactic:
]

Goal state after:
case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
⊢ normalizer ↑P ≤ centralizer ↑P
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
⊢ ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) =
    (Trivialization.linearMapAt ℝ (trivializationAt ℝ (fun x ↦ ℝ) x) y)
      (((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y 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
⊢ ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) =
    (Trivialization.linearMapAt ℝ (trivializationAt ℝ (fun x ↦ ℝ) x) y)
      (((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w))
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} = closure (⇑H.subtype '' {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆})

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆} = closure (⇑H.subtype '' {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆})
Module: Mathlib.GroupTheory.Focal

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.commutator ↥H ≤ closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup ≤ H.focalSubgroup

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inl
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime 1

Tactic:
]

Goal state after:
case neg.inl
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime 1
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:
]

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)))
⊢ ∏ 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
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))

Tactic:
]

Goal state after:
case neg.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ¬(Nat.card G).minFac ∣ (↑P).index

Tactic:
]

Goal state after:
case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ¬(Nat.card G).minFac ∣ (↑P).index
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
g : ↥P
hQ : IsPGroup p (↥↑P ⧸ (↑P).focalSubgroupOf)
⊢ ↑g ^ (↑P).index = 1 ↔ g ∈ (↑P).focalSubgroupOf

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
g : ↥P
hQ : IsPGroup p (↥↑P ⧸ (↑P).focalSubgroupOf)
⊢ ↑g ^ (↑P).index = 1 ↔ g ∈ (↑P).focalSubgroupOf
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ map (↑P).subtype ((↑P).transferFocal.domRestrict ↑P).ker = map (↑P).subtype (↑P).focalSubgroupOf

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ map (↑P).subtype ((↑P).transferFocal.domRestrict ↑P).ker = map (↑P).subtype (↑P).focalSubgroupOf
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ⊤

Tactic:
]

Goal state after:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ⊤
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G

Tactic:
]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
q : Group.IsNilpotent ↥(frattini G) ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
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' y) w) w ≤ r' ^ 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
⊢ ((g' y) w) w ≤ r' ^ 2 * ((g' x) w) w
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
]

Goal state after:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ ((∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, x.1 = y.1 → x.2 = y.2)
        (replicate (n + 1) (head :: tail))) ∧
    ∀ a ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?,
      ∀ b ∈ (replicate (n + 1) (head :: tail)).flatten.head?, a.1 = b.1 → a.2 = b.2

Tactic:
]

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ ((∀ l ∈ replicate (n + 1) (head :: tail), IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) l) ∧
      IsChain (fun l₁ l₂ ↦ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, x.1 = y.1 → x.2 = y.2)
        (replicate (n + 1) (head :: tail))) ∧
    ∀ a ∈ (replicate (n + 1) (head :: tail)).flatten.getLast?,
      ∀ b ∈ (replicate (n + 1) (head :: tail)).flatten.head?, a.1 = b.1 → a.2 = b.2
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2

Tactic:
]

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : (head :: tail).head? = some x✝
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2

Tactic:
]

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : (head :: tail).head? = some x✝
⊢ x✝¹.1 = x✝.1 → x✝¹.2 = x✝.2
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₁ ++ L₂ ++ (replicate n L₂).flatten)

Tactic:
]

Goal state after:
case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₁ ++ L₂ ++ (replicate n L₂).flatten)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten

Tactic:
]

Goal state after:
case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_2
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)

Tactic:
]

Goal state after:
case refine_2
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_2
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten

Tactic:
]

Goal state after:
case refine_2
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (replicate (n + 1) L₂).flatten
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : IsReduced l → IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
⊢ IsCyclicallyReduced (reduceCyclically (a :: (l ++ [b])))

Tactic:
reduceCyclically.cons_append

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : IsReduced l → IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
⊢ IsCyclicallyReduced (if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b])