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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup : (cs.rightInvSeq ω)[j]? = (cs.rightInvSeq ω)[j']?
j'_lt_length : j' < ω.length
⊢ j < (cs.rightInvSeq ω).length

Tactic:
simp

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'
dup : (cs.rightInvSeq ω)[j]? = (cs.rightInvSeq ω)[j']?
j'_lt_length : j' < ω.length
⊢ j < ω.length
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : some (cs.rightInvSeq ω)[j] = (cs.rightInvSeq ω)[j']?
⊢ j' < (cs.rightInvSeq ω).length

Tactic:
simp

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : some (cs.rightInvSeq ω)[j] = (cs.rightInvSeq ω)[j']?
⊢ j' < ω.length
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j' 1 = 1

Tactic:
dup

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
⊢ ↑0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
⊢ ∀ (x y : M), ↑(x + y) = ↑x + ↑y

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : ℚ≥0
m : M
s : ℕ+
⊢ a.den ∈ nonZeroDivisors ℕ

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m n : M
h : ↑s • m = ↑s • n
⊢ ↑s ≠ 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
induction b with | mk mb sb

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
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hbc : mk mb sb ≤ c
hab : mk ma sa ≤ mk mb sb
⊢ 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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : ↑sb • ma ≤ ↑sa • mb
mc : M
sc : ℕ+
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sb ≠ 0

Tactic:
simp

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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hab : ↑sb • ma ≤ ↑sa • mb
mc : M
sc : ℕ+
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sc ≠ 0

Tactic:
simp

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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
mc : M
sc : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sa ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
induction b with | mk mb sb

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 : ℕ+
h : mk ma sa ≤ mk mb sb
h' : mk mb sb ≤ mk ma sa
⊢ mk ma sa = mk mb sb
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
induction b with | mk mb sb

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 : ℕ+
⊢ mk ma sa ≤ mk mb sb ∨ mk mb sb ≤ mk ma sa
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
induction b with | mk mb sb

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
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ mk ma sa + mk mb sb < 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 : ℚ≥0
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c

Tactic:
induction b with | mk mb sb

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
a : ℚ≥0
ha : 0 < a
c : DivisibleHull M
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ a • mk mb sb < a • c
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : 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
i : ι
⊢ (FreeGroup.lift a) (FreeGroup.of i) =
    ((lift fun i ↦ FreeGroup.lift fun x ↦ a i).comp freeGroupEquivCoprodI.toMonoidHom) (FreeGroup.of i)

Tactic:
simp

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
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ 0 < ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(leftRel K)) q = Quot.mk (⇑(leftRel K)) x
a' : ↥K.op
ha' : (fun m ↦ m • x) a' = q
⊢ (↑a')⁻¹ ∈ K.op

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ArchimedeanClass.mk (↑↑s • mk m s) = ArchimedeanClass.mk (↑↑s' • mk m s')
⊢ ↑↑s ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (↑↑s' • mk m s')
⊢ ↑↑s' ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : ↑a * x = q
⊢ (↑a)⁻¹ ∈ H

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
x : G
⊢ (domRestrictHom (OrderDual.ofDual ((fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker) H)) Mˣ)
        ((monoidHomMonoidHomEquiv G M).symm x) =
      1 ↔
    x ∈ H

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
φ : G →* Mˣ
⊢ (∀ x ∈ (fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ, φ x = 1) ↔
    φ ∈ OrderDual.ofDual Φ

Tactic:
simp

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✝ : Finite α
⊢ IsFinitelyPresented (FreeGroup α)

Tactic:
have ⟨n, _, f, hf_surj, hf_inj⟩ := Finite.exists_equiv_fin α
  refine ⟨n, FreeGroup.map f, FreeGroup.map_surjective hf_surj.surjective, ?_⟩
  · rw [(FreeGroup.map f).ker_eq_bot (FreeGroup.map_injective hf_inj.injective)]
    exact .bot

Goal state after:
Module: Mathlib.GroupTheory.Focal

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (fun g ↦ g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆) = fun x ↦ ∃ a ∈ {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}, H.subtype a = x

Tactic:
simp

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (fun g ↦ g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆) = fun x ↦ (∃ x_1 ∈ H, ∃ u, x = ⁅x_1, u⁆) ∧ x ∈ H
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
⊢ ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) =
    (Trivialization.linearMapAt ℝ (trivializationAt ℝ (fun x ↦ ℝ) x) y)
      (((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w))

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Radical

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ ∀ (x : α), ⨅ (_ : f.toEquiv x ∈ {H | IsCoatom H}), f.toEquiv x = ⨅ (_ : x ∈ {H | IsCoatom H}), f x

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n : ℕ
x✝ : List (α × Bool)
h : IsCyclicallyReduced x✝
⊢ IsCyclicallyReduced (replicate 0 x✝).flatten

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
h : IsCyclicallyReduced []
⊢ IsCyclicallyReduced (replicate (n + 1) []).flatten

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
⊢ [] ∉ replicate (n + 1) (head :: tail)

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
h : IsCyclicallyReduced L
n : ℕ
⊢ IsCyclicallyReduced (replicate n L).flatten

Tactic:
match n, L with
  | 0, _ => simp
  | n + 1, [] => simp
  | n + 1, (head :: tail) =>
    rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]
    refine ⟨⟨by simpa [IsReduced] using h.isReduced, List.isChain_replicate_of_rel _ h.2⟩,
      fun _ ha _ hb ↦ ?_⟩
    rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha
    rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb
    exact h.2 _ ha _ hb

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
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ ((g' y) w) w = ((g' y - g' x) w) w + ((g' x) w) w

Tactic:
simp

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ [] ++ (L₁ ++ L₂) ++ L₃ = L₁ ++ L₂ ++ L₃

Tactic:
simp

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ L₁ ++ (L₂ ++ L₃) ++ [] = L₁ ++ L₂ ++ L₃

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced []
⊢ IsCyclicallyReduced (reduceCyclically [])

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a✝ : α × Bool
h : IsReduced [a✝]
⊢ IsCyclicallyReduced (reduceCyclically [a✝])

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
⊢ conjugator [] ++ reduceCyclically [] ++ invRev (conjugator []) = []

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a✝ : α × Bool
⊢ conjugator [a✝] ++ reduceCyclically [a✝] ++ invRev (conjugator [a✝]) = [a✝]

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
h✝ : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ [] ++ (a :: l ++ [b]) ++ invRev [] = a :: (l ++ [b])

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
y : G
⊢ ⁅1, y⁆ ∈ N

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
h₁✝ : IsCyclicallyReduced (reduceCyclically L)
h₂✝ : IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))
⊢ n + 1 + 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
⊢ reduce (replicate 0 L).flatten =
    if 0 = 0 then [] else conjugator L ++ (replicate 0 (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w w' : α × Bool
h : ∀ (x : FreeGroup α), x.toWord[0]? = some w → ¬w = w'
⊢ (mk [w]).toWord[0]? = some w

Tactic:
simp

Goal state after: