mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
⊢ (lift FreeGroup.of).comp (FreeGroup.lift of) = MonoidHom.id (FreeGroup X)

Tactic:
apply FreeGroup.ext_hom

Goal state after:
ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H : Type u_4
inst✝² : Group G✝
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
⊢ ∀ (a : X),
    ((lift FreeGroup.of).comp (FreeGroup.lift of)) (FreeGroup.of a) = (MonoidHom.id (FreeGroup X)) (FreeGroup.of a)
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2

Tactic:
← A,

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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖(Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
          Trivialization.symmL ℝ (trivializationAt F E x) x) ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2
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
w : W
i : B
⊢ cs.IsRightInversion w (cs.simple i) ↔ cs.IsRightDescent w i

Tactic:
by
  simp [IsRightInversion, IsRightDescent, cs.isReflection_simple i]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ cons m ls h1 h2 = of m • ls

Tactic:
rw [of_smul_def, equivPair_eq_of_fstIdx_ne _]
  · simp [cons, rcons, h2]
  · exact h1

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).last⟩ ∈ (singleton x✝ a✝).toList.getLast?

pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨j✝, _w₁✝.last⟩ ∈ _w₁✝.toList.getLast?
_w₂_ih✝ : ⟨l✝, _w₂✝.last⟩ ∈ _w₂✝.toList.getLast?
⊢ ⟨l✝, (_w₁✝.append _hne✝ _w₂✝).last⟩ ∈ (_w₁✝.append _hne✝ _w₂✝).toList.getLast?

Tactic:
· rw [Option.mem_def]
    rfl

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨j✝, _w₁✝.last⟩ ∈ _w₁✝.toList.getLast?
_w₂_ih✝ : ⟨l✝, _w₂✝.last⟩ ∈ _w₂✝.toList.getLast?
⊢ ⟨l✝, (_w₁✝.append _hne✝ _w₂✝).last⟩ ∈ (_w₁✝.append _hne✝ _w₂✝).toList.getLast?
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.tail
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

Tactic:
exact ih mem

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
rcases hcard with hcard | hcard

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

case inr
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : ∃ i, 3 ≤ #(H i)
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
subst hh

Goal state after:
case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hl : j = i
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
subst hh

Goal state after:
case neg
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hl : ¬j = i
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
⊢ mk ma sa ≤ mk mb sb ∨ mk mb sb ≤ mk ma sa

Tactic:
simp_rw [mk_le_mk]

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
⊢ ↑sb • ma ≤ ↑sa • mb ∨ ↑sa • mb ≤ ↑sb • ma
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)
⊢ (FreeGroup.lift fun x ↦ of ((B x.fst) x.snd)).comp (lift fun i ↦ (B i).lift fun x ↦ FreeGroup.of ⟨i, x⟩) =
    MonoidHom.id (CoprodI G)

Tactic:
ext1 i; apply (B i).ext_hom; simp

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 ↦ x1 * x2) g r ∈ H
⊢ r * (↑⟨r, hr⟩)⁻¹ ∈ ↑H

pp: case py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 ↦ x1 * x2) g r ∈ H
⊢ r * (↑⟨1, hR1⟩)⁻¹ ∈ ↑H

Tactic:
· rw [Subtype.coe_mk, mul_inv_cancel]
    exact H.one_mem

Goal state after:
case py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 ↦ x1 * x2) g r ∈ H
⊢ r * (↑⟨1, hR1⟩)⁻¹ ∈ ↑H
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h : Group.FG ↥N
⊢ N.IsFinitelyNormallyGenerated

Tactic:
by
  obtain ⟨S, rfl, hS⟩ := N.fg_iff.mp ((Group.fg_iff_subgroup_fg N).mp h)
  exact ⟨S, hS, le_antisymm (normalClosure_le_normal subset_closure) closure_le_normalClosure⟩

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
⊢ (QuotientGroup.mk' H.focalSubgroupOf) ⟨g⁻¹ * h * g, hconj⟩ = (QuotientGroup.mk' H.focalSubgroupOf) ⟨h, hh⟩

Tactic:
apply QuotientGroup.eq.mpr

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.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
⊢ (↑P).transferFocal.ker ⊓ ↑P = (↑P).focalSubgroup

Tactic:
rw [← subgroupOf_map_subtype, ← MonoidHom.ker_domRestrict, ← map_focalSubgroupOf]

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.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ⁅upperCentralSeries G (n + 1), ⊤⁆ ≤ upperCentralSeries G n

Tactic:
by
  apply closure_le _ |>.mpr
  rintro _ ⟨h, hh, g, _, rfl⟩
  exact mem_upperCentralSeries_succ_iff.mp hh g

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (nilpotencyClass G) = ⊥

Tactic:
← lowerCentralSeries_length_eq_nilpotencyClass

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (Nat.find ⋯) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ nilpotencyClass G ≤ n

Tactic:
← lowerCentralSeries_length_eq_nilpotencyClass

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ Nat.find ⋯ ≤ n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass ↥H ≤ nilpotencyClass G

Tactic:
← lowerCentralSeries_length_eq_nilpotencyClass

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G

Tactic:
← lowerCentralSeries_length_eq_nilpotencyClass

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
← lowerCentralSeries_length_eq_nilpotencyClass

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

Tactic:
← lowerCentralSeries_length_eq_nilpotencyClass

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
by_cases hG : IsNilpotent G
  · intros a ha b hb ab
    simp only [Set.mem_Iic] at ha hb
    apply lt_of_le_of_ne
    · exact upperCentralSeries_mono _ ab.le
    · grind only [IsNilpotent.nilpotent', IsNilpotent.nilpotent, eq_top,
        upperCentralSeries_eq_top_iff_nilpotencyClass_le]
  · rw [nilpotencyClass_of_not_nilpotent hG, ← Nat.bot_eq_zero, Set.Iic_bot]
    apply Set.strictMonoOn_singleton

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 : α
⊢ N ⊔ IwaS.T a = ⊤

Tactic:
rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]

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.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:
IwaS.is_conj g a

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₂
⊢ g ∈ H

Tactic:
rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2]

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
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
hB_ne : B.Nonempty
⊢ B.ncard * (orbit G B).ncard = Nat.card X

Tactic:
obtain ⟨x, hx⟩ := hB_ne
  rw [ncard_block_eq_relIndex hB hx, ← index_stabilizer,
      Subgroup.relIndex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive]

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

Tactic:
rw [← isSimpleOrder_blockMem_iff_isPreprimitive G a, ← Set.isSimpleOrder_Ici_iff_isCoatom]

Goal state after:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder (BlockMem G a)
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
suffices b ∉ B by
    rw [Set.mem_iInter] at this
    simpa only [Set.mem_iInter, not_forall, exists_prop] using this

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case «0»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 0
ha : Even 0
h2 : g.cycleType = Multiset.replicate 0 2
h✝ : 0 * 2 ≤ card (Fin 5)
h : 0 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 0 2

pp: case «1»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 1
ha : Even 1
h2 : g.cycleType = Multiset.replicate 1 2
h✝ : 1 * 2 ≤ card (Fin 5)
h : 1 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 1 2

pp: case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

pp: case «3»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 3
ha : Even 3
h2 : g.cycleType = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 3 2

Tactic:
· exact (h1 (card_cycleType_eq_zero.1 h_1)).elim

Goal state after:
case «1»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 1
ha : Even 1
h2 : g.cycleType = Multiset.replicate 1 2
h✝ : 1 * 2 ≤ card (Fin 5)
h : 1 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 1 2

case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

case «3»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 3
ha : Even 3
h2 : g.cycleType = Multiset.replicate 3 2
h✝ : 3 * 2 ≤ card (Fin 5)
h : 3 ≤ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 3 2
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : g • aux x = aux y
⊢ ∃ g, g • x = y

Tactic:
use σ g

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := ⋯
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : g • aux x = aux y
⊢ σ g • x = y
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F‖ <
    2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)

Tactic:
← A,

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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
          Trivialization.symmL ℝ (trivializationAt F E x) x‖ <
    2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ map Perm.ofSubtype (alternatingGroup ↥s) = Perm.ofSubtype.range ⊓ alternatingGroup α

Tactic:
map_ofSubtype

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Perm.ofSubtype.range ⊓ alternatingGroup α = Perm.ofSubtype.range ⊓ alternatingGroup α