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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨j, w.last⟩ ∈ w.toList.getLast?

Tactic:
induction w

Goal state after:
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?

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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j : ι
w : NeWord M i j
⊢ ∀ l ∈ w.toList, l.snd ≠ 1

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ∀ l ∈ (singleton x✝ a✝).toList, l.snd ≠ 1

case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
⊢ ∀ l ∈ (_w₁✝.append _hne✝ _w₂✝).toList, l.snd ≠ 1
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
i j : ι
w : NeWord M i j
⊢ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w.toList

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (singleton x✝ a✝).toList

case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
⊢ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (_w₁✝.append _hne✝ _w₂✝).toList
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case left
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t

pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)

Tactic:
· exact cs.isReflection_of_mem_leftInvSeq ω ht

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.length (t * cs.wordProd ω) < cs.length (cs.wordProd ω)
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 < j' → j' < (cs.rightInvSeq ω).length → (cs.rightInvSeq ω)[j]? ≠ (cs.rightInvSeq ω)[j']?

Tactic:
j_lt_j'

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' < (cs.rightInvSeq ω).length → (cs.rightInvSeq ω)[j]? ≠ (cs.rightInvSeq ω)[j']?
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
x : M i
hnotone : x ≠ 1
w : NeWord M i j
⊢ (replaceHead x hnotone w).head = x

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (singleton x✝ a✝)).head = x

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✝ : ∀ (x : M i✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₁✝).head = x
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₂✝).head = x
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (_w₁✝.append _hne✝ _w₂✝)).head = x
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head ≠ 1
⊢ (w.mulHead x hnotone).head = x * w.head

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x * (singleton x✝ a✝).head ≠ 1
⊢ ((singleton x✝ a✝).mulHead x hnotone).head = x * (singleton x✝ a✝).head

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✝ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (_w₁✝.mulHead x hnotone).head = x * _w₁✝.head
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (_w₂✝.mulHead x hnotone).head = x * _w₂✝.head
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ ((_w₁✝.append _hne✝ _w₂✝).mulHead x hnotone).head = x * (_w₁✝.append _hne✝ _w₂✝).head
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv.prod = w.prod⁻¹

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ : ι
x✝ : G i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).inv.prod = (singleton x✝ a✝).prod⁻¹

case append
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord G i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord G k✝ l✝
_w₁_ih✝ : _w₁✝.inv.prod = _w₁✝.prod⁻¹
_w₂_ih✝ : _w₂✝.inv.prod = _w₂✝.prod⁻¹
⊢ (_w₁✝.append _hne✝ _w₂✝).inv.prod = (_w₁✝.append _hne✝ _w₂✝).prod⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv.head = w.last⁻¹

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ : ι
x✝ : G i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).inv.head = (singleton x✝ a✝).last⁻¹

case append
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord G i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord G k✝ l✝
_w₁_ih✝ : _w₁✝.inv.head = _w₁✝.last⁻¹
_w₂_ih✝ : _w₂✝.inv.head = _w₂✝.last⁻¹
⊢ (_w₁✝.append _hne✝ _w₂✝).inv.head = (_w₁✝.append _hne✝ _w₂✝).last⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv.last = w.head⁻¹

Tactic:
induction w

Goal state after:
case singleton
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ : ι
x✝ : G i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).inv.last = (singleton x✝ a✝).head⁻¹

case append
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord G i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord G k✝ l✝
_w₁_ih✝ : _w₁✝.inv.last = _w₁✝.head⁻¹
_w₂_ih✝ : _w₂✝.inv.last = _w₂✝.head⁻¹
⊢ (_w₁✝.append _hne✝ _w₂✝).inv.last = (_w₁✝.append _hne✝ _w₂✝).head⁻¹
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ (QuotientGroup.rightRel H) a b

Tactic:
QuotientGroup.rightRel_apply

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
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 ι
⊢ Function.Injective ⇑(lift f)

Tactic:
apply (injective_iff_map_eq_one (lift f)).mpr

Goal state after:
ι : 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 ι
⊢ ∀ (a : CoprodI H), (lift f) a = 1 → a = 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
x : DivisibleHull M
x✝³ x✝² : M
x✝¹ x✝ : ℕ+
h : mk x✝³ x✝¹ = mk x✝² x✝
⊢ ArchimedeanClass.mk x✝³ = ArchimedeanClass.mk x✝²

Tactic:
apply aux_archimedeanClassOrderHom_injective

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
x : DivisibleHull M
x✝³ x✝² : M
x✝¹ x✝ : ℕ+
h : mk x✝³ x✝¹ = mk x✝² x✝
⊢ (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝³) = (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝²)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : DecidableEq G
R S : Finset G
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ↑(Finset.image (fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤

Tactic:
by
  rw [Finset.coe_image, Finset.coe_mul]
  exact closure_mul_image_eq_top hR hR1 hS

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
⊢ Group.IsNilpotent G → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G

Tactic:
· rintro ⟨n, nH⟩
    exact ⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G
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 : ∃ n, ⊤.lowerCentralSeries n = ⊥
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥

Tactic:
rcases hG with ⟨n, hG⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
n : ℕ
hG : ⊤.lowerCentralSeries n = ⊥
⊢ ∃ n, ⊤.lowerCentralSeries n = ⊥
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
h : Function.Surjective ⇑f
n : ℕ
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n

Tactic:
induction n with
  | zero => simp
  | succ d hd =>
    rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
    rcases h y' with ⟨y, rfl⟩
    simpa using! hd (mem_map_of_mem f (hx y))

Goal state after:
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
h : Function.Surjective ⇑f
n : ℕ
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n

Tactic:
by
  induction n with
  | zero => simp
  | succ d hd =>
    rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
    rcases h y' with ⟨y, rfl⟩
    simpa using! hd (mem_map_of_mem f (hx y))

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))⁻¹ =
    1

Tactic:
@mul_inv_eq_one _ _ (f _)

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.GroupAction.Blocks

Goal state before:
pp: case inl
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.Injective ⇑f
B : Set β
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f ⁻¹' B)

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.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
· apply Or.intro_left; exact Set.Subsingleton.preimage hB hf

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.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (x : G), ¬x • B = ∅

Tactic:
intro g hg

Goal state after:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ False
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
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ IsBlockSystem G (range fun g ↦ g • B)

Tactic:
refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
  case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g
  · simp only [Set.mem_range, not_exists]
    intro g hg
    apply hBe.ne_empty
    simpa only [Set.smul_set_eq_empty] using hg
  · intro a
    obtain ⟨b : X, hb : b ∈ B⟩ := hBe
    obtain ⟨g, rfl⟩ := exists_smul_eq G b a
    use g • B
    simp only [Set.smul_mem_smul_set_iff, hb, Set.mem_range,
      exists_apply_eq_apply, and_imp, forall_exists_index,
      forall_apply_eq_imp_iff, true_and]
    exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩

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

Goal state before:
pp: X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B = Set.univ

Tactic:
B.eq_univ_iff_ncard

Goal state after:
X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
⊢ Nat.card ↥(ofStabilizer G a) + 1 = Nat.card α

Tactic:
by
  classical
  let := Fintype.ofFinite α
  rw [Nat.subtype_card {a}ᶜ, ← Finset.card_singleton a, Finset.card_compl_add_card,
    Nat.card_eq_fintype_card]
  simp [mem_ofStabilizer_iff]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
⊢ IsPretransitive (↥N) α

Tactic:
by
    rw [Set.ne_univ_iff_exists_notMem] at hNX
    obtain ⟨a, ha⟩ := hNX
    rw [isPretransitive_iff_orbit_eq_univ a]
    apply Or.resolve_left (isTrivialBlock_of_isBlock (IsBlock.orbit_of_normal a))
    intro h
    apply ha
    simp only [mem_fixedPoints]
    intro n
    rw [← Set.mem_singleton_iff]
    suffices orbit N a = {a} by rw [← this]; use n
    ext b
    rw [Set.Subsingleton.eq_singleton_of_mem h (MulAction.mem_orbit_self a)]

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

Goal state before:
pp: case inl
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
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
g : G
⊢ a ∈ ⋂ (_ : a ∈ g • A), g • A

Tactic:
simp only [Set.mem_iInter, imp_self]

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ {g | g.cycleType = {2, 2}} ⊆ ↑(alternatingGroup α)

Tactic:
intro g hg

Goal state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg : g ∈ {g | g.cycleType = {2, 2}}
⊢ g ∈ ↑(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ {g | g.cycleType = {2, 2}} ⊆ ↑(alternatingGroup α)

Tactic:
intro g hg

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ {g | g.cycleType = {2, 2}}
⊢ g ∈ ↑(alternatingGroup α)
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✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
⊢ 0 ≤ RCLike.re (((g.inner b) v) v)

Tactic:
rcases eq_or_ne v 0 with rfl | hv

Goal state after:
case inl
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✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
⊢ 0 ≤ RCLike.re (((g.inner b) 0) 0)

case inr
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✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
hv : v ≠ 0
⊢ 0 ≤ RCLike.re (((g.inner b) v) v)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
ha : (Classical.choice Hs) i = a
⊢ g • (append x) (castAdd m i) = ↑((Classical.choice Hs) i)

Tactic:
rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]

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

Goal state before:
pp: case zero
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hn : IsMultiplyPreprimitive M α 0
hmn : m ≤ 0
hα : ↑0 ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α m

Tactic:
rw [Nat.eq_zero_of_le_zero hmn]; exact hn

Goal state after:
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
g' : α
⊢ g' ∈ ofSubtype g • s ↔ g' ∈ s

Tactic:
mem_smul_set,

Goal state after:
α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
g' : α
⊢ (∃ y ∈ s, ofSubtype g • y = g') ↔ g' ∈ s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
⊢ G = ⊤

Tactic:
suffices IsPreprimitive G α from subgroup_eq_top_of_isPreprimitive hα G hG.le

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
⊢ IsPreprimitive (↥G) α
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝ : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial ↥G
⊢ G = ⊤

Tactic:
apply Subgroup.eq_top_of_le_card

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝ : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial ↥G
⊢ Nat.card (Perm α) ≤ Nat.card ↥G
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝ : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial ↥G
⊢ 2 ≤ Nat.card ↥G

Tactic:
Nat.succ_le_iff,

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝ : Finite α
hα : Nat.card α ≤ 2
hG : Nontrivial ↥G
⊢ 1 < Nat.card ↥G
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
⊢ ∀ (g : G), (∀ (a : ↑(powersetCard α n)), g +ᵥ a = a) → g = 0

Tactic:
intro g hg

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
G : Type u_3
inst✝² : AddGroup G
inst✝¹ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulVAdd G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g +ᵥ a = a
⊢ g = 0
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
⊢ ∀ (g : G), (∀ (a : ↑(powersetCard α n)), g • a = a) → g = 1

Tactic:
intro g hg

Goal state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
inst✝ : FaithfulSMul G α
g : G
hg : ∀ (a : ↑(powersetCard α n)), g • a = a
⊢ g = 1