mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Blocks

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

Tactic:
simp only [← hk, inv_smul_smul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
a✝ : Nontrivial α
⊢ alternatingGroup α = ⊥

Tactic:
suffices hα' : Nat.card α = 2 by
    rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by simp),
      two_mul_nat_card_alternatingGroup, mul_one, Nat.card_perm, hα', Nat.factorial_two]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
a✝ : Nontrivial α
⊢ Nat.card α = 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : Perm α
⊢ k ∈ map Perm.ofSubtype (alternatingGroup ↥s) ↔ k ∈ Perm.ofSubtype.range ⊓ alternatingGroup α

Tactic:
rw [Subgroup.mem_map, Subgroup.mem_inf, MonoidHom.mem_range]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
k : Perm α
⊢ (∃ x ∈ alternatingGroup ↥s, Perm.ofSubtype x = k) ↔ (∃ x, Perm.ofSubtype x = k) ∧ k ∈ alternatingGroup α
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y‖ < 2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)

Tactic:
grw [this, ← A, ← comp_assoc, opNorm_comp_le]

Goal state after:
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ *
      ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖ <
    2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ (MulAut.conj g)⁻¹ • k ∈ (ofSubtype s).range ↔ k ∈ (ofSubtype (g • s)).range

Tactic:
mem_range_ofSubtype_iff,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
g k : ↥(alternatingGroup α)
⊢ (↑((MulAut.conj g)⁻¹ • k)).support ⊆ s ↔ (↑k).support ⊆ g • s
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✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
⊢ ContinuousAt (fun v ↦ ((g.inner b) v) v) 0

Tactic:
by
    -- Continuity of bilinear maps is only true on normed spaces. As `F` is a normed space by
    -- assumption, we transfer everything to `F` and argue there.
    let e : E b ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E b) _
      (FiberBundle.mem_baseSet_trivializationAt' b)
    let m : (E b →L[ℝ] E b →L[ℝ] ℝ) ≃L[ℝ] (F →L[ℝ] F →L[ℝ] ℝ) :=
      e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
    have A (v : E b) : g.inner b v v = ((fun w ↦ m (g.inner b) w w) ∘ e) v := by simp [m]
    simp only [A]
    fun_prop

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

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h0 : n = 0
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
rw [h0]

Goal state after:
case inl
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : IsPretransitive M α
n : ℕ
a : α
inst✝ : IsMultiplyPreprimitive M α n.succ
h0 : n = 0
⊢ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) 0
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : s.ncard = sᶜ.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

pp: case inr.inr
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
· contrapose hα
    rw [← Set.ncard_add_ncard_compl s, two_mul, ← h]

Goal state after:
case inr.inr
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (stabilizer (Perm α) s)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝³ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this✝² : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
this✝¹ : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
this✝ : ¬B ⊆ s
this : ¬B ⊆ sᶜ
⊢ sᶜ ⊆ B

Tactic:
apply hB.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
      hG.le

Goal state after:
case hBs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝³ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this✝² : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
this✝¹ : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
this✝ : ¬B ⊆ s
this : ¬B ⊆ sᶜ
⊢ ¬B ⊆ s

case hBsc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝³ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < G
this✝² : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
this✝¹ : IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1)
this✝ : ¬B ⊆ s
this : ¬B ⊆ sᶜ
⊢ ¬B ⊆ sᶜ
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
⊢ 2 ≤ Nat.card ↥φ.range

Tactic:
by_contra H

Goal state after:
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
H : ¬2 ≤ Nat.card ↥φ.range
⊢ False
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
s✝ t : ↑(powersetCard α n)
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : ↑(powersetCard α n)
⊢ (compl hm) (g • s) = id g • (compl hm) s

Tactic:
by ext; simp [← inv_smul_mem_iff]

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
x : α
hx : x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
hg' : ⟨g, hg⟩ ∈ fixingSubgroup (↥G) (↑g.support)ᶜ
g' : ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) := ⟨⟨g, hg⟩, hg'⟩
i : ℤ
hi : (g ^ i) a = x
⊢ ∃ k, x = k • a

Tactic:
exact ⟨g' ^ i, hi.symm⟩

Goal state after:
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
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
⊢ (lift f x hx) t = x

Tactic:
by
  delta HNNExtension; simp [lift, t]

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G},
    (∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤) → H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), ((F i).subgroupOf (F (i + 1))).Normal
ih1 : F (n + 1) = ⊤
⊢ (F 0).IsSubnormal

Tactic:
refine step _ _ (hF <| Nat.le_add_right 0 1) ?_ (H_le _)

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G},
    (∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤) → H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), ((F i).subgroupOf (F (i + 1))).Normal
ih1 : F (n + 1) = ⊤
⊢ (F (0 + 1)).IsSubnormal
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑b.2 * (↑c.2 * a.1) ≤ ↑b.2 * (↑a.2 * c.1)

Tactic:
grw [mul_left_comm, hab]

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑a.2 * b.1) ≤ ↑b.2 * (↑a.2 * c.1)
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_2
α : 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
z : α
hz : z ∈ {x | Equiv.swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

pp: case refine_3
α : 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
⊢ y ∈ {x | Equiv.swap x y ∈ closure S}

Tactic:
· exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z y⟩

Goal state after:
case refine_3
α : 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
⊢ y ∈ {x | Equiv.swap x y ∈ closure S}
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 : α
h1 : f b = f a
⊢ a ∈ orbit (↥(closure S)) a

Tactic:
apply mem_orbit_self

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} * n = (card α).choose n * n !

Tactic:
← Nat.mul_left_inj (factorial_ne_zero _),

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} * n * ?m.83! = (card α).choose n * n ! * ?m.83!

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ ℕ
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case inl
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i✝ : ι
p : Pair d i✝
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i✝).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.tail.toList
⊢ g ∈ d.set i

pp: case inr
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
p : Pair d i
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
left✝ : ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ≠ 1
⊢ ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ∈ d.set i

Tactic:
· exact p.normalized _ _ hg

Goal state after:
case inr
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
p : Pair d i
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
left✝ : ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ≠ 1
⊢ ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ∈ d.set i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ (2 * (Nat.factorization 2) 2 + (Nat.factorization 3) 2) = 4

Tactic:
Nat.prime_two.factorization_self,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ (2 * 1 + (Nat.factorization 3) 2) = 4
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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
⊢ head₁ = head₂ ∧ tail₁ = tail₁

Tactic:
rw [← equiv_fst_mul_equiv_snd (d.compl i) head₁,
      ← equiv_fst_mul_equiv_snd (d.compl i) head₂,
    h₁, h₃]

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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
⊢ ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 = ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 ∧ tail₁ = tail₁
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:
by
    have : IsMulCommutative (alternatingGroup s) := isMulCommutative_of_card_le_three (by simp)
    infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {b | (↑b).IsThreeCycle} = ⊤

Tactic:
rw [← closure_three_cycles_eq_alternating]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {b | (↑b).IsThreeCycle} = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ (ofSubtype s) σ ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔
    (↑((ofSubtype s) σ)).support ⊆ s ∧ (↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2})

Tactic:
simp_rw [and_iff_right hk, Subgroup.mem_map, ofSubtype_inj, existsAndEq, and_true,
      ← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hs]

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ σ ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}} ↔ ↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ k * a 1 = a ↑(k + 1)

Tactic:
IH,

Goal state after:
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a ↑k * a 1 = a ↑(k + 1)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
⊢ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) =
    MulAut.conj ⟨g, hg⟩ • Subgroup.map (ofSubtype s) (kleinFour ↥s)

Tactic:
ext ⟨k, hk⟩

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    ⟨k, hk⟩ ∈ MulAut.conj ⟨g, hg⟩ • Subgroup.map (ofSubtype s) (kleinFour ↥s)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / (2 * n).gcd i.val

Tactic:
by
  conv_lhs => rw [← ZMod.natCast_zmod_val i]
  rw [← a_one_pow, orderOf_pow, orderOf_a_one]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Nat.card G ∣ Monoid.exponent G

Tactic:
rw [← Nat.factorization_prime_le_iff_dvd Nat.card_pos.ne' Monoid.exponent_ne_zero_of_finite]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (p : ℕ), Nat.Prime p → (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsZGroup G ↔ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
by
  refine ⟨fun hG ↦ ?_, ?_⟩
  · obtain ⟨H, hH⟩ := Subgroup.exists_right_complement'_of_coprime hG.coprime_commutator_index
    have h1 : Abelianization G ≃* H := hH.symm.QuotientMulEquiv
    refine ⟨commutator G, H, _, (SemidirectProduct.mulEquivSubgroup hH).symm,
      isCyclic_of_surjective _ h1.surjective, hG.isCyclic_commutator, ?_⟩
    exact Nat.card_congr h1.toEquiv ▸ hG.coprime_commutator_index
  · rintro ⟨N, H, φ, e, hH, hN, hHN⟩
    have : IsZGroup (N ⋊[φ] H) :=
      isZGroup_of_coprime SemidirectProduct.range_inl_eq_ker_rightHom.ge hHN
    exact IsZGroup.of_injective (f := e.toMonoidHom) e.injective

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ ((Measure.dirac (a, a)).bind ⇑(swap α α)) s = (Measure.dirac (a, a)) s

Tactic:
Measure.dirac_bind (Kernel.measurable _),

Goal state after:
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ ((swap α α) (a, a)) s = (Measure.dirac (a, a)) s
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
a : α
s : Set α
hs : MeasurableSet s
⊢ ((κ ^ (n + m)) a) s = ∫⁻ (b : α), ((κ ^ n) b) s ∂(κ ^ m) a

Tactic:
simp [pow_add, comp_apply' _ _ _ hs]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β), g c ∂κ.fst a = ∫⁻ (bc : β × γ), g bc.1 ∂κ a

Tactic:
by
  rw [fst_eq, lintegral_map _ measurable_fst a hg]

Goal state after: