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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ f (stabilizerEquiv_invFun_aux g • a) = f a

Tactic:
Perm.smul_def

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ f ((stabilizerEquiv_invFun_aux g) a) = f a
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
a : ↥A
x✝ : NormalWord d
⊢ (unitsSMulEquiv φ * (MulAction.toPermHom G (NormalWord d)) ↑a) x✝ =
    ((MulAction.toPermHom G (NormalWord d)) ↑(φ a) * unitsSMulEquiv φ) x✝

Tactic:
simp [unitsSMul_one_group_smul]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t ^ ↑1 • w = unitsSMul φ 1 w

pp: case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t ^ ↑(-1) • w = unitsSMul φ (-1) w

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t ^ ↑1 • w = unitsSMul φ 1 w

case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t ^ ↑(-1) • w = unitsSMul φ (-1) w
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
x y z : α
h : z ∈ {x, y}ᶜ
⊢ z ≠ x

pp: case a
α : Type u_2
inst✝ : DecidableEq α
x y z : α
h : z ∈ {x, y}ᶜ
⊢ z ≠ y

Tactic:
<;>

Goal state after:
case a
α : Type u_2
inst✝ : DecidableEq α
x y z : α
h : z ∈ {x, y}ᶜ
⊢ z ≠ x

case a
α : Type u_2
inst✝ : DecidableEq α
x y z : α
h : z ∈ {x, y}ᶜ
⊢ z ≠ y
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case a
α : Type u_2
inst✝ : DecidableEq α
y z : α
h : z ∈ {z, y}ᶜ
⊢ False

pp: case a
α : Type u_2
inst✝ : DecidableEq α
x z : α
h : z ∈ {x, z}ᶜ
⊢ False

Tactic:
<;>

Goal state after:
case a
α : Type u_2
inst✝ : DecidableEq α
y z : α
h : z ∈ {z, y}ᶜ
⊢ False

case a
α : Type u_2
inst✝ : DecidableEq α
x z : α
h : z ∈ {x, z}ᶜ
⊢ False
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons.h1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).head = (cons g u w h1 h2).head

pp: case h2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).toList[i✝]? = some a✝ ↔ (cons g u w h1 h2).toList[i✝]? = some a✝

Tactic:
<;>

Goal state after:
case cons.h1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).head = (cons g u w h1 h2).head

case h2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
i✝ : ℕ
a✝ : ℤˣ × G
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).toList[i✝]? = some a✝ ↔ (cons g u w h1 h2).toList[i✝]? = some a✝
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_4.inl
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
w : α
hzw : a ≠ w
hσ : Equiv.swap a w ∈ S
hσa : Equiv.swap a w • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ Equiv.swap (Equiv.swap a w • a) a ∈ closure S

pp: case refine_4.inr
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z : α
hzw : z ≠ a
hσ : Equiv.swap z a ∈ S
hσa : Equiv.swap z a • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ Equiv.swap (Equiv.swap z a • a) a ∈ closure S

Tactic:
<;>

Goal state after:
case refine_4.inl
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
w : α
hzw : a ≠ w
hσ : Equiv.swap a w ∈ S
hσa : Equiv.swap a w • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ Equiv.swap (Equiv.swap a w • a) a ∈ closure S

case refine_4.inr
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z : α
hzw : z ≠ a
hσ : Equiv.swap z a ∈ S
hσa : Equiv.swap z a • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ Equiv.swap (Equiv.swap z a • a) a ∈ closure S
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
⊢ Equiv.swap x y ∈ closure S ↔ x ∈ orbit (↥(closure S)) y

Tactic:
by
  refine ⟨fun h ↦ ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩
  by_contra h
  have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
  · obtain ⟨σ, hσ, a, ha, hσa⟩ := this
    obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ
    have := ne_of_mem_of_not_mem ha hσa
    rw [Perm.smul_def, ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at this
    refine hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha)
    obtain rfl | rfl := this <;> simpa [Equiv.swap_comm] using subset_closure hσ
  · obtain ⟨x, y, -, rfl⟩ := hS f hf; rwa [swap_inv]
  · exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z y⟩
  · rw [mem_ofPred, Equiv.swap_self]; apply one_mem

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
h : b = a
⊢ a = b

pp: case neg
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
h : ¬b = a
⊢ b = b

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
h : b = a
⊢ a = b

case neg
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
h : ¬b = a
⊢ b = b
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
x✝ : Q
⊢ (a * b * c).left x✝ = (a * (b * c)).left x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
⊢ (a * b * c).right = (a * (b * c)).right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
x✝ : Q
⊢ (a * b * c).left x✝ = (a * (b * c)).left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
⊢ (a * b * c).right = (a * (b * c)).right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (1 * a).left x✝ = a.left x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (1 * a).right = a.right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (1 * a).left x✝ = a.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (1 * a).right = a.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a * 1).left x✝ = a.left x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a * 1).right = a.right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a * 1).left x✝ = a.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a * 1).right = a.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a⁻¹ * a).left x✝ = left 1 x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a⁻¹ * a).right = right 1

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a⁻¹ * a).left x✝ = left 1 x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a⁻¹ * a).right = right 1
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝² x✝¹ x✝ : Q
⊢ { left := 1, right := x✝² * x✝¹ }.left x✝ = ({ left := 1, right := x✝² } * { left := 1, right := x✝¹ }).left x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ }.right = ({ left := 1, right := x✝¹ } * { left := 1, right := x✝ }).right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝² x✝¹ x✝ : Q
⊢ { left := 1, right := x✝² * x✝¹ }.left x✝ = ({ left := 1, right := x✝² } * { left := 1, right := x✝¹ }).left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ }.right = ({ left := 1, right := x✝¹ } * { left := 1, right := x✝ }).right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
x✝ : Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
          ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).left
      x✝ =
    x.left x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
        ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).right =
    x.right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
x✝ : Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
          ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).left
      x✝ =
    x.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
        ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).right =
    x.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
x✝ : Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
          ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).left
      x✝ =
    x.left x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
        ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).right =
    x.right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
x✝ : Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
          ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).left
      x✝ =
    x.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
        ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).right =
    x.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
x✝ : Q₂
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.left x✝ =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).left
      x✝

pp: case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.right =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } *
        { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).right

Tactic:
<;>

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
x✝ : Q₂
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.left x✝ =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).left
      x✝

case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.right =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } *
        { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).right
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case hinj
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ (i : ↥g.cycleFactorsFinset), Function.Injective ⇑((fun c ↦ zpowers ↑c) i).subtype

Tactic:
· exact fun i ↦ subtype_injective _

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))

Tactic:
if_pos hm.1,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
⊢ K = ⊥ ∨ K = ⊤

Tactic:
conv at key =>
    rhs
    rhs
    rw [← N.range_subtype, N.subtype.range_eq_map]

Goal state after:
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤
⊢ K = ⊥ ∨ K = ⊤
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁✝ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1
this : h₁⁻¹ * h₂ = 1
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }

Tactic:
inv_mul_eq_one

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁✝ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1
this : h₁ = h₂
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case «0»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
hg0 : (-1) ^ (g.cycleType.sum + 0) = 1
h1 : 0 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 0 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

pp: case «1»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
hg0 : (-1) ^ (g.cycleType.sum + 1) = 1
h1 : 1 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 1 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

pp: case «2»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
hg0 : (-1) ^ (g.cycleType.sum + 2) = 1
h1 : 2 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 2 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Tactic:
<;>

Goal state after:
case «0»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
hg0 : (-1) ^ (g.cycleType.sum + 0) = 1
h1 : 0 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 0 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

case «1»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
hg0 : (-1) ^ (g.cycleType.sum + 1) = 1
h1 : 1 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 1 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}

case «2»
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
hg0 : (-1) ^ (g.cycleType.sum + 2) = 1
h1 : 2 ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate 2 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case h_one_le
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

pp: case hn
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 2 < Nat.card α

pp: case hα
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 2

Tactic:
<;>

Goal state after:
case h_one_le
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

case hn
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ 2 < Nat.card α

case hα
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ↑(Set.powersetCard α 3)
⊢ IsMulCommutative ↥(ofSubtype ↑s).range

Tactic:
have : IsMulCommutative (alternatingGroup s) := isMulCommutative_of_card_le_three (by simp)
    infer_instance

Goal state after: