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

Goal state before:
pp: case succ
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.wordProd (alternatingWord i i' (m + 1)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
rw [alternatingWord_succ', wordProd_cons, ih]
    by_cases hm : Even m
    · have h₁ : ¬ Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]
      simp [hm, h₁, h₂]
    · have h₁ : Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
      simp [hm, h₁, h₂, ← pow_succ', ← mul_assoc]

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

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ Even (↑(M.M i i') * 2 - 2 * k)

Tactic:
by use -k + (M i i'); ring

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inr.nil
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (i ≠ j ∧ ∃ (h : [] ≠ []), [].head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ []

pp: case inr.cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
head✝ : (i : ι) × M i
tail✝ : List ((i : ι) × M i)
⊢ (i ≠ j ∧ ∃ (h : head✝ :: tail✝ ≠ []), (head✝ :: tail✝).head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ head✝ :: tail✝

Tactic:
<;>

Goal state after:
case inr.nil
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (i ≠ j ∧ ∃ (h : [] ≠ []), [].head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ []

case inr.cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
head✝ : (i : ι) × M i
tail✝ : List ((i : ι) × M i)
⊢ (i ≠ j ∧ ∃ (h : head✝ :: tail✝ ≠ []), (head✝ :: tail✝).head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ head✝ :: tail✝
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:
by
  rw [Nat.sub_le_iff_le_add]; exact length_le_length_mul_add_left ..

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

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

pp: case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length w < cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
<;>

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length w < cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
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

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:
<;>

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

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
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
    simp

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

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
    simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x : DivisibleHull M
f : M → ℕ+ → α
h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s'
p p' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨u, hu⟩ := heq

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x : DivisibleHull M
f : M → ℕ+ → α
h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s'
p p' : M × ↥(nonZeroDivisors ℕ)
u : ↥(nonZeroDivisors ℕ)
hu : u • p'.2 • p.1 = u • p.2 • p'.1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
heq' : q ≈ q'
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨u, hu⟩ := heq

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq' : q ≈ q'
u : ↥(nonZeroDivisors ℕ)
hu : u • p'.2 • p.1 = u • p.2 • p'.1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.GroupTheory.CoprodI

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

pp: 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⁻¹

Tactic:
<;>

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: 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⁻¹

pp: 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⁻¹

Tactic:
<;>

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: 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⁻¹

pp: 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⁻¹

Tactic:
<;>

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

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
x : DivisibleHull M
⊢ (a + b) • x = a • x + b • x

Tactic:
by
    induction x with | mk m s
    simp_rw [qsmul_mk, mk_add_mk, mk_eq_mk]
    use 1
    suffices ((a + b).num * a.den * b.den * (s * s)) • m =
        ((a.num * b.den + b.num * a.den) * (a + b).den * (s * s)) • m by
      convert! this using 1
      all_goals
      simp [← natCast_zsmul, smul_smul, ← add_smul]
      ring_nf
    rw [Rat.add_num_den']

Goal state after:
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
⊢ (lift f) w.prod ≠ 1

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
⊢ (lift f) w.prod ≠ 1

Tactic:
<;>

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
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
⊢ (lift f) w.prod ≠ 1

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
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_1.e'_3
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑t • m = (↑s * ↑t) • ↑t' • m'

pp: case e'_1.e'_4
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑s • n = (↑s * ↑t) • ↑s' • n'

Tactic:
· simp_rw [smul_smul, mul_rotate s'.val, ← smul_smul, h, smul_smul]
    ring_nf

Goal state after:
case e'_1.e'_4
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑s • n = (↑s * ↑t) • ↑s' • n'
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
I : Finset (Quotient ↑H ↑K)
hI : ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ
⊢ ↑I = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
I : Finset (Quotient ↑H ↑K)
hI : ∀ (x : G), x ∈ ⋃ i ∈ I, quotToDoubleCoset H K i
⊢ ∀ (x : Quotient ↑H ↑K), x ∈ ↑I
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_3.e'_5
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sc * ↑sb) = ↑sa * ↑sb * ↑sc

pp: case e'_3.e'_6
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sc * ↑sa) = ↑sa * ↑sa * ↑sc

pp: case e'_4.e'_5
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sb * ↑sc) = ↑sa * ↑sb * ↑sc

pp: case e'_4.e'_6
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sb * ↑sa) = ↑sa * ↑sa * ↑sb

Tactic:
<;>

Goal state after:
case e'_3.e'_5
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sc * ↑sb) = ↑sa * ↑sb * ↑sc

case e'_3.e'_6
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sc * ↑sa) = ↑sa * ↑sa * ↑sc

case e'_4.e'_5
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sb * ↑sc) = ↑sa * ↑sb * ↑sc

case e'_4.e'_6
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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sc) • mb < (↑sa * ↑sb * ↑sc) • ma + (↑sa * ↑sa * ↑sb) • mc
⊢ ↑sa * (↑sb * ↑sa) = ↑sa * ↑sa * ↑sb
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_3
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
⊢ c.den * ↑s * b.num = b.num * c.den * ↑s

pp: case e'_4
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.den * ↑s * c.num = c.num * b.den * ↑s

Tactic:
<;>

Goal state after:
case e'_3
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
⊢ c.den * ↑s * b.num = b.num * c.den * ↑s

case e'_4
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.den * ↑s * c.num = c.num * b.den * ↑s
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hXdisj.hs
ι : 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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) ((fun i ↦ X i ∪ Y i) j)

pp: case hXdisj.ht
ι : 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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) ((fun i ↦ X i ∪ Y i) j)

Tactic:
<;>

Goal state after:
case hXdisj.hs
ι : 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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) ((fun i ↦ X i ∪ Y i) j)

case hXdisj.ht
ι : 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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) ((fun i ↦ X i ∪ Y i) j)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ { toFun := fun g ↦ diff ϕ default (g • default), map_one' := ⋯, map_mul' := ⋯ } g = diff ϕ ?R (g • ?R)

pp: case R
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ H.LeftTransversal

Tactic:
<;>

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ { toFun := fun g ↦ diff ϕ default (g • default), map_one' := ⋯, map_mul' := ⋯ } g = diff ϕ ?R (g • ?R)

case R
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ H.LeftTransversal
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)

Tactic:
by
  -- First handle the case when `Z(G)` has infinite index and `[G : Z(G)]` is defined to be `0`
  by_cases hG : (center G).index = 0
  · simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero]
  have : FiniteIndex (center G) := ⟨hG⟩
  -- Rewrite as `|Z(G) ∩ G'| * [G' : Z(G) ∩ G'] ∣ [G : Z(G)] ^ ([G : Z(G)] * n) * [G : Z(G)]`
  rw [← ((center G).subgroupOf (_root_.commutator G)).card_mul_index, pow_succ]
  -- We have `h1 : [G' : Z(G) ∩ G'] ∣ [G : Z(G)]`
  have h1 := relIndex_dvd_index_of_normal (center G) (_root_.commutator G)
  -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n)`
  refine mul_dvd_mul ?_ h1
  -- We know that `[G' : Z(G) ∩ G'] < ∞` by `h1` and `hG`
  have : FiniteIndex ((center G).subgroupOf (_root_.commutator G)) :=
    ⟨ne_zero_of_dvd_ne_zero hG h1⟩
  -- We have `h2 : rank (Z(G) ∩ G') ≤ [G' : Z(G) ∩ G'] * rank G'` by Schreier's lemma
  have h2 := rank_le_index_mul_rank ((center G).subgroupOf (_root_.commutator G))
  -- We have `h3 : [G' : Z(G) ∩ G'] * rank G' ≤ [G : Z(G)] * n` by `h1` and `rank G' ≤ n`
  have h3 := Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1) (rank_commutator_le_card G)
  -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ rank (Z(G) ∩ G')`
  refine dvd_trans ?_ (pow_dvd_pow (center G).index (h2.trans h3))
  -- `Z(G) ∩ G'` is abelian, so it enough to prove that `g ^ [G : Z(G)] = 1` for `g ∈ Z(G) ∩ G'`
  apply card_dvd_exponent_pow_rank'
  intro g
  -- `Z(G)` is abelian, so `g ∈ Z(G) ∩ G' ≤ G' ≤ ker (transfer : G → Z(G))`
  have := Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G) g.1.2
  -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done
  simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using! this

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
⊢ g * n * g⁻¹ ∈ H.focalSubgroup

Tactic:
induction hn using closure_induction with

Goal state after:
Module: Mathlib.GroupTheory.Focal

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

Tactic:
rw [focalSubgroup_def, closure_le]
  rintro g ⟨_, x, _, u, rfl⟩
  exact commutator_mem_commutator (mem_top x) (mem_top u)

Goal state after: