mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → AddCommGroup (V x)
inst✝³ : (x : M) → Module 𝕜 (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst✝ : Fintype ι
hs : IsLocalFrameOn I F n s u
t : (x : M) → V x
hx : x ∈ u
⊢ t x = ∑ i, (hs.coeff i x) (t x) • s i x

Tactic:
by
  simpa [coeff, hx] using (Basis.sum_repr (hs.toBasisAt hx) (t x)).symm

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
x : G
⊢ x * x = 1

Tactic:
by
  rw [mul_eq_one_iff_eq_inv, inv_eq_self]

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

Goal state before:
pp: case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n / n.gcd m.val ∣ lcm n 2

Tactic:
refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)

Goal state after:
case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n = n / n.gcd m.val * gcd n m.val
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
⊢ ∀ (f : G →* H) (a : X), lift.symm f a = f (of a)

Tactic:
f

Goal state after:
ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
⊢ ∀ (a : X), lift.symm f a = f (of a)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
K : Type u_3
inst✝ : Group K
f : G →* K
g : H →* K
⊢ (lift f g).range = f.range ⊔ g.range

Tactic:
by
  simp [range_eq]

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
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
⊢ p w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w
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
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w
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
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w
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.simple (if Even m then i' else i) * cs.wordProd (alternatingWord i i' m) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
ih

Goal state after:
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.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
by
  suffices cs.lengthParity (t * w) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, this]
  rcases ht with ⟨w, i, rfl⟩
  simp [lengthParity_simple]

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
ω : List B
ih : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) :: cs.rightInvSeq (ω.concat i) =
    (List.map (⇑(MulAut.conj (cs.simple i)))
          ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω :: cs.rightInvSeq ω)).concat
      (cs.simple i)

Tactic:
ih

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
ω : List B
ih : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i) =
    (List.map (⇑(MulAut.conj (cs.simple i)))
          ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω :: cs.rightInvSeq ω)).concat
      (cs.simple i)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω) =
    ((List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse)).concat (cs.simple i)).reverse

Tactic:
ih

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse).reverse =
    ((List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse)).concat (cs.simple i)).reverse
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ of ((equivPair i) w).head • ((equivPair i) w).tail = w

Tactic:
← rcons_eq_smul,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ rcons ((equivPair i) w) = w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ w.prod • empty = w → (of m • w).prod • empty = of m • w

Tactic:
ih

Goal state after:
case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : w.prod • empty = w
⊢ (of m • w).prod • empty = of m • w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : w.prod • empty = w
⊢ of m • w.prod • empty = of m • w

Tactic:
ih

Goal state after:
case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : w.prod • empty = w
⊢ of m • w = of m • w
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
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse

Tactic:
List.take_reverse

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
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
j : ℕ
⊢ (cs.rightInvSeq (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
List.take_reverse

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ (∃ u, u • ↑ⁿ s' • m = u • ↑ⁿ s • m') ↔ ∃ u, ↑u • ↑s' • m = ↑u • ↑s • m'

Tactic:
↑ⁿ.exists_congr_left

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ (∃ u, u • ↑ⁿ s' • m = u • ↑ⁿ s • m') ↔ ∃ b, ↑(↑ⁿ.symm b) • ↑s' • m = ↑(↑ⁿ.symm b) • ↑s • m'
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) ∧ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * b * y
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y

Tactic:
obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
i : Quotient ↑H ↑K
a : G
hg : a ∈ quotToDoubleCoset H K i
⊢ mk H K a = i

Tactic:
simp [mk_eq_of_doubleCoset_eq (doubleCoset_eq_of_mem hg)]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

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

pp: case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ I, ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ) → Finite (Quotient ↑H ↑K)

Tactic:
· intro _
    cases nonempty_fintype (Quotient (H : Set G) K)
    exact ⟨Finset.univ, by simpa using! iUnion_quotToDoubleCoset _ _⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ I, ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ) → Finite (Quotient ↑H ↑K)
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ˣ
⊢ φ ∈
      OrderDual.ofDual
        ((fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker)
          ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ)) ↔
    φ ∈ OrderDual.ofDual Φ

Tactic:
OrderDual.ofDual_toDual,

Goal state after:
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ˣ
⊢ φ ∈
      (domRestrictHom
          ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ) Mˣ).ker ↔
    φ ∈ OrderDual.ofDual Φ
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ˣ)
g : G
⊢ g ∈ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual (OrderDual.toDual Φ)) Mˣ).ker ↔
    ∀ φ ∈ Φ, φ g = 1

Tactic:
OrderDual.ofDual_toDual,

Goal state after:
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ˣ)
g : G
⊢ g ∈ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom Φ Mˣ).ker ↔ ∀ φ ∈ Φ, φ g = 1
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s)) ∈ ↑(closure U) * R

Tactic:
refine Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ r * s * (↑(f (r * s)))⁻¹ ∈ closure U
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 : ℕ
hn : n ≠ 0
⊢ IsReduced (L₁ ++ (replicate n L₂).flatten ++ L₃)

Tactic:
by
  match n with
  | 0 => contradiction
  | n + 1 =>
    if h : L₂ = [] then simp_all else
    have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]
    refine IsReduced.append_overlap ?_ ?_ (hn := h')
    · rw [replicate_succ, flatten_cons, ← append_assoc]
      refine IsReduced.append_overlap (h₂.infix ⟨[], L₃, by simp⟩) ?_ h
      rw [← flatten_cons, ← replicate_succ]
      exact (h₁.flatten_replicate _).isReduced
    · rw [replicate_succ', flatten_concat]
      refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h
      rw [← flatten_concat, ← replicate_succ']
      exact (h₁.flatten_replicate _).isReduced

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

Goal state before:
pp: G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
⊢ ∀ (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g

Tactic:
f

Goal state after:
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
⊢ ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
⊢ x = y

Tactic:
classical
    let f (a : FreeGroup α) (n : ℕ) : ℕ :=
        (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length +
          (conjugator a.toWord).length)
    let g (a : FreeGroup α) (k : ℕ) : List (α × Bool) :=
        conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++
          invRev (conjugator a.toWord))
    have heq₂ : x ^ (2 * n) = y ^ (2 * n) := by simp_rw [mul_comm, pow_mul, heq]
    replace heq : g x n = g y n := by
      simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq
    replace heq₂ : g x (2 * n) = g y (2 * n) := by
      simpa [toWord_pow, reduce_flatten_replicate, isReduced_toWord, hn] using congr_arg toWord heq₂
    have leq : f x n = f y n := by simpa [g] using congr_arg List.length heq
    have leq₂ : f x (2 * n) = f y (2 * n) := by simpa [g] using congr_arg List.length heq₂
    obtain ⟨hc, heq'⟩ := List.append_inj heq (by grind)
    obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    have hm : reduceCyclically x.toWord = reduceCyclically y.toWord := by
      simp only [replicate_succ, flatten_cons, append_assoc] at heq'
      exact (List.append_inj heq' <| mul_left_cancel₀ hn <| by grind).1
    have := congr_arg mk <| (conj_conjugator_reduceCyclically x.toWord).symm
    rwa [hc, hm, conj_conjugator_reduceCyclically, mk_toWord, mk_toWord] at this

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

Goal state before:
pp: G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
⊢ ∀ (f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X),
    ∃! F, ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a

Tactic:
f

Goal state after:
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
⊢ ∃! F, ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
ih

Goal state after:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
⊢ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
⊢ H = ⊤

Tactic:
let H' := H.map (mk' (center G))

Goal state after:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H = ⊤
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • c • ↑s = b • c • ↑s

Tactic:
← smul_assoc,

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ (a • c) • ↑s = b • c • ↑s
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • d • ↑s = b • c • ↑s

Tactic:
smul_coe_set hc,

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ b • d • ↑s = b • ↑s
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • op c • ↑s = b • op c • ↑s

Tactic:
← smul_assoc,

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ (a • op c) • ↑s = b • op c • ↑s
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ iSup IwaS.T ≤ N ⊔ IwaS.T a

Tactic:
iSup_le_iff

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
this : g ∈ H
⊢ g • orbit (↥H) a = orbit (↥H) a

Tactic:
← Subgroup.coe_mk H g this,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
this : g ∈ H
⊢ ↑⟨g, this⟩ • orbit (↥H) a = orbit (↥H) a