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
⊢ dist (g' y) (g' x) ≤ δ

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
⊢ dist (g' y) (g' x) ≤ δ
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 ω * 1

Tactic:
;

Goal state after:
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 ω * 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
;

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k < 2 * p
⊢ k < 2 * p

Tactic:
;

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k < 2 * p
⊢ k < 2 * p
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑⊥ ↑H) a✝ b✝ ↔ (leftRel H) a✝ b✝

Tactic:
← bot_rel_eq_leftRel H

Goal state after:
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
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis (X i) (G i)
a✝ : (i : ι) × X i
⊢ ((lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩).comp (FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)))
      (FreeGroup.of a✝) =
    (MonoidHom.id (FreeGroup ((i : ι) × X i))) (FreeGroup.of a✝)

Tactic:
;

Goal state after:
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝² : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis (X i) (G i)
a✝ : (i : ι) × X i
⊢ ((lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩).comp (FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)))
      (FreeGroup.of a✝) =
    (MonoidHom.id (FreeGroup ((i : ι) × X i))) (FreeGroup.of a✝)
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
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis (X i) (G i)
i : ι
⊢ ((FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)).comp (lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩)).comp of =
    (MonoidHom.id (CoprodI G)).comp of

Tactic:
;

Goal state after:
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝² : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis (X i) (G i)
i : ι
⊢ ((FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)).comp (lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩)).comp of =
    (MonoidHom.id (CoprodI G)).comp of
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
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis (X i) (G i)
i : ι
⊢ ∀ (i_1 : X i),
    (((FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)).comp (lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩)).comp of)
        ((B i) i_1) =
      ((MonoidHom.id (CoprodI G)).comp of) ((B i) i_1)

Tactic:
;

Goal state after:
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝² : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
ι : Type u_4
X : ι → Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
B : (i : ι) → FreeGroupBasis (X i) (G i)
i : ι
⊢ ∀ (i_1 : X i),
    (((FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)).comp (lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩)).comp of)
        ((B i) i_1) =
      ((MonoidHom.id (CoprodI G)).comp of) ((B i) i_1)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case refine_3
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
a✝ : ι
⊢ ((lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i).comp (FreeGroup.lift fun i ↦ of (FreeGroup.of ())))
      (FreeGroup.of a✝) =
    (MonoidHom.id (FreeGroup ι)) (FreeGroup.of a✝)

Tactic:
;

Goal state after:
case refine_3
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
a✝ : ι
⊢ ((lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i).comp (FreeGroup.lift fun i ↦ of (FreeGroup.of ())))
      (FreeGroup.of a✝) =
    (MonoidHom.id (FreeGroup ι)) (FreeGroup.of a✝)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
i : ι
a : Unit
⊢ (((FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i)).comp of)
      (FreeGroup.of a) =
    ((MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)).comp of) (FreeGroup.of a)

Tactic:
;

Goal state after:
case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
i : ι
a : Unit
⊢ (((FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i)).comp of)
      (FreeGroup.of a) =
    ((MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)).comp of) (FreeGroup.of a)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case refine_4.unit
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
i : ι
⊢ (((FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i)).comp of)
      (FreeGroup.of PUnit.unit) =
    ((MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)).comp of) (FreeGroup.of PUnit.unit)

Tactic:
;

Goal state after:
case refine_4.unit
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
i : ι
⊢ (((FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i)).comp of)
      (FreeGroup.of PUnit.unit) =
    ((MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)).comp of) (FreeGroup.of PUnit.unit)
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
this : ‖(Trivialization.symmL ℝ (trivializationAt F E x) y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2
⊢ ‖(Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
            Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x)
          v‖ ^
      2 ≤
    (r' * ‖v‖) ^ 2

Tactic:
by simpa [mul_pow]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝² x✝¹ : G
x✝ : G →* Mˣ
⊢ ↑(((Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) (x✝² * x✝¹)) x✝) =
    ↑(((Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝² *
          (Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝¹)
        x✝)

Tactic:
;

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝² x✝¹ : G
x✝ : G →* Mˣ
⊢ ↑(((Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) (x✝² * x✝¹)) x✝) =
    ↑(((Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝² *
          (Equiv.ofBijective (fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) x✝¹)
        x✝)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i • (Y i)ᶜ ⊆ X i

Tactic:
;

Goal state after:
case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i • (Y i)ᶜ ⊆ X i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ (a i)⁻¹ • (X i)ᶜ ⊆ Y i

Tactic:
;

Goal state after:
case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ (a i)⁻¹ • (X i)ᶜ ⊆ Y i
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.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic

Tactic:
;

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝ : Group G
S T : Subgroup G
h : S ≤ T
⊢ (fun S ↦ S.lowerCentralSeries 0) S ≤ (fun S ↦ S.lowerCentralSeries 0) T

Tactic:
;

Goal state after:
case zero
G : Type u_1
inst✝ : Group G
S T : Subgroup G
h : S ≤ T
⊢ (fun S ↦ S.lowerCentralSeries 0) S ≤ (fun S ↦ S.lowerCentralSeries 0) T
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
S T : Subgroup G
h : S ≤ T
⊢ (fun S ↦ S.lowerCentralSeries (d + 1)) S ≤ (fun S ↦ S.lowerCentralSeries (d + 1)) T

Tactic:
;

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
S T : Subgroup G
h : S ≤ T
⊢ (fun S ↦ S.lowerCentralSeries (d + 1)) S ≤ (fun S ↦ S.lowerCentralSeries (d + 1)) T
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
S T : Subgroup G
h : S ≤ T
⊢ ⁅S.lowerCentralSeries d, S⁆ ≤ ⁅T.lowerCentralSeries d, T⁆

Tactic:
;

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
d : ℕ
hd : Monotone fun S ↦ S.lowerCentralSeries d
S T : Subgroup G
h : S ≤ T
⊢ ⁅S.lowerCentralSeries d, S⁆ ≤ ⁅T.lowerCentralSeries d, T⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal

Tactic:
;

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Group.IsNilpotent ↥H

Tactic:
rw [nilpotent_iff_lowerCentralSeries] at *
  rcases hG with ⟨n, hG⟩
  refine ⟨n, ?_⟩
  rw [← map_subtype_inj, map_bot, top_subtype_lowerCentralSeries, eq_bot_iff, ← hG]
  exact H.lowerCentralSeries_mono n le_top

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

Goal state before:
pp: case refine_1.cons.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ f' e = 1

Tactic:
exact dif_pos (Or.inl eT)

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
obtain ⟨e, he⟩ := goursat_surjective hI₁' hI₂'

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ inst✝ : H₁.Normal
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ inst✝ : H₁.Normal
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))
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 - g' x‖ * (‖w‖ * ‖w‖) + ((g' x) w) w ≤ δ * (‖w‖ * ‖w‖) + ((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 - g' x‖ * (‖w‖ * ‖w‖) + ((g' x) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' x) w) w