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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
        if i = j then 1
        else
          if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4
          else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).transpose =
    Matrix.of fun i j ↦
      if i = j then 1
      else if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Matrix

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Matrix.of
          (fun i j ↦
            if i = j then 1
            else
              if ↑i = n - 1 ∧ ↑j = n - 2 ∨ ↑j = n - 1 ∧ ↑i = n - 2 then 4
              else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2)
          i i' ≠
        1

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Matrix

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
        if i = j then 1
        else
          if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
          else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).transpose =
    Matrix.of fun i j ↦
      if i = j then 1
      else if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Matrix

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ ∀ (i i' : Fin n),
    i ≠ i' →
      Matrix.of
          (fun i j ↦
            if i = j then 1
            else
              if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
              else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2)
          i i' ≠
        1

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Matrix

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else m + 2).transpose = Matrix.of fun i j ↦ if i = j then 1 else m + 2

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)

Tactic:
rw [Nat.sub_le_iff_le_add]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)

Tactic:
rw [Nat.sub_le_iff_le_add]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ (take j ω).length + (drop j ω).length = ω.length

Tactic:
by rw [← List.length_append, ω.take_append_drop j]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append.inl
ι : 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 : (i : ι) × M i
h✝ : l ∈ _w₁✝.toList
⊢ l.snd ≠ 1

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append.inr
ι : 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 : (i : ι) × M i
h✝ : l ∈ _w₂✝.toList
⊢ l.snd ≠ 1

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: 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

Tactic:
· intro l h
      simp only [toList, List.mem_append] at h
      cases h <;> aesop

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : ℕ
m : M
s : ℕ+
⊢ a • mk m s = mk (a • m) s

Tactic:
induction a with

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : DivisibleHull M
⊢ a ≤ a

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m : M
s : ℕ+
⊢ mk m s ≤ mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b c : DivisibleHull M
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
hbc : b ≤ c
ma : M
sa : ℕ+
hab : mk ma sa ≤ b
⊢ mk ma sa ≤ c
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b : DivisibleHull M
h : a ≤ b
h' : b ≤ a
⊢ a = b

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
h : mk ma sa ≤ b
h' : b ≤ mk ma sa
⊢ mk ma sa = b
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b : DivisibleHull M
⊢ a ≤ b ∨ b ≤ a

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
⊢ mk ma sa ≤ b ∨ b ≤ mk ma sa
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b c : DivisibleHull M
h : b < c
⊢ a + b < a + c

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
h : b < c
ma : M
sa : ℕ+
⊢ mk ma sa + b < mk ma sa + c
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ≥0
h : b < c
⊢ b • a < c • a

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ b • mk m s < c • mk m s
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
a b : DivisibleHull M
h : ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b
⊢ a.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
induction a with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
b : DivisibleHull M
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝ den✝) ≤ ArchimedeanClass.mk b
⊢ (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ArchimedeanClass (DivisibleHull M)
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) a = OrderHom.id a

Tactic:
induction a with

Goal state after:
case h₁.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk a) =
    OrderHom.id (ArchimedeanClass.mk a)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk a) =
    OrderHom.id (ArchimedeanClass.mk a)

Tactic:
induction a with

Goal state after:
case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk (mk m s)) =
    OrderHom.id (ArchimedeanClass.mk (mk m s))
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₂
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : ArchimedeanClass M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) a = OrderHom.id a

Tactic:
induction a with

Goal state after:
case h₂.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a✝ : M
⊢ ((archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M)) (ArchimedeanClass.mk a✝) =
    OrderHom.id (ArchimedeanClass.mk a✝)
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 ^ (-1) • (X i)ᶜ ⊆ Y i

Tactic:
zpow_neg,

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 ^ 1)⁻¹ • (X i)ᶜ ⊆ Y i
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 * (↑⟨1, hR1⟩)⁻¹ ∈ ↑H

Tactic:
rw [Subtype.coe_mk, inv_one, mul_one]
    exact (H.mul_mem_cancel_left (hU hg)).mp hh

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : IsFinitelyPresented G
inst✝ : IsFinitelyPresented H
⊢ IsFinitelyPresented (Monoid.Coprod G H)

Tactic:
obtain ⟨_, sG, ⟨_ : Finite sG, ⟨φG⟩⟩⟩ := exists_mulEquiv_presentedGroup (G := G)
  obtain ⟨_, sH, ⟨_ : Finite sH, ⟨φH⟩⟩⟩ := exists_mulEquiv_presentedGroup (G := H)
  exact equiv ((PresentedGroup.coprodPresentations sG sH).trans (MulEquiv.coprodCongr φG φH).symm)

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * ⁅x, u⁆ * g⁻¹ ∈ H

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x : G
hxP : x ∈ H
u : G
hzH : ⁅x, u⁆ ∈ H
⊢ g * x * g⁻¹ ∈ H

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ ↑y * ↑x✝ = ↑x✝ * ↑y

Tactic:
← QuotientGroup.mk_mul,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ ↑(y * x✝) = ↑x✝ * ↑y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ ↑(y * x✝) = ↑x✝ * ↑y

Tactic:
← QuotientGroup.mk_mul,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ ↑(y * x✝) = ↑(x✝ * y)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsDescendingCentralSeries ⊤.lowerCentralSeries

Tactic:
constructor
  · rfl
  intro x n hxn g
  exact commutator_mem_commutator hxn (mem_top g)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ (k • g).support = ConjAct.ofConjAct k • g.support

Tactic:
by
  ext
  rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ (MulAut.conj k).symm c ∈ g.cycleFactorsFinset

Tactic:
← mem_cycleFactorsFinset_conj g k

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ k • B' = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

Tactic:
hkB'

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ B' = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
⊢ IsPreprimitive H Y

Tactic:
refine ⟨fun {B} hB ↦ ?_⟩

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G ∅ = ⊤

Tactic:
aesop

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
⊢ stabilizer G univ = ⊤

Tactic:
aesop

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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hn : l.length = 2 * (n + 1)
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
rw [Nat.mul_succ] at hn
    obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.length_cons, Nat.succ_inj] at hn
    obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
    rw [List.prod_cons, List.prod_cons, ← mul_assoc]
    apply mul_mem <;> grind [IsSwap.mul_mem_closure_three_cycles]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : ⇑(alternatingGroup α).subtype '' {x | ↑x ∈ {g | g.IsThreeCycle}} = {g | g.IsThreeCycle}
⊢ closure (⇑(alternatingGroup α).subtype '' {g | (↑g).IsThreeCycle}) = map (alternatingGroup α).subtype ⊤

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
this✝ : ⇑(alternatingGroup α).subtype '' {x | ↑x ∈ {g | g.cycleType = {2, 2}}} = {g | g.cycleType = {2, 2}}
this : closure {g | g.cycleType = {2, 2}} = alternatingGroup α
⊢ closure (⇑(alternatingGroup α).subtype '' {g | (↑g).cycleType = {2, 2}}) = map (alternatingGroup α).subtype ⊤

Tactic:
aesop

Goal state after:
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
⊢ ∃ C > 0, ∀ᶠ (y : B) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt F E x) y‖ < C

Tactic:
by
  refine ⟨2 * (1 + ‖(trivializationAt F E x).symmL ℝ x‖), by positivity, ?_⟩
  filter_upwards [eventually_norm_symmL_trivializationAt_comp_self_lt F E x one_lt_two] with y hy
  have A : ((trivializationAt F E x).continuousLinearMapAt ℝ x) ∘L
      ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
    ext v
    have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      mem_baseSet_trivializationAt, comp_apply, id_apply]
    convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
  have : (trivializationAt F E x).symmL ℝ y =
     ((trivializationAt F E x).symmL ℝ y) ∘L (ContinuousLinearMap.id _ _) := by simp
  grw [this, ← A, ← comp_assoc, opNorm_comp_le]
  gcongr
  linarith

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
inst✝ : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : ↑n ≤ ENat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact IsPretransitive.of_surjective_map
    (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_ENatCard hα) inferInstance

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ G

Tactic:
eq_alternatingGroup_of_index_eq_two (hG.antisymm h)

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
h✝ : G.index > 0
h : Nat.succ 0 < G.index
⊢ alternatingGroup α ≤ alternatingGroup α
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ Function.Injective ⇑(stabilizer G a).subtype

Tactic:
by simp only [Subgroup.coe_subtype, Subtype.coe_injective]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ : Set α
hs : s✝.encard + 1 = ↑0
⊢ IsPreprimitive ↥(fixingSubgroup M s✝) ↥(ofFixingSubgroup M s✝)

Tactic:
simp at hs

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

Goal state before:
pp: case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
⊢ ↑b = ↑c

Tactic:
obtain ⟨h, hinvab⟩ := exists_smul_eq G (b : α) a

Goal state after:
case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
this : IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)
g : G
hg : g ∈ stabilizer G a
hgbc : ↑(⟨g, hg⟩ • b) = ↑c
h : G
hinvab : h • ↑b = a
⊢ ↑b = ↑c
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = ↑n
⊢ a ∉ Subtype.val '' s

Tactic:
aesop

Goal state after: