mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
⊢ ∀ (x y : G₁), e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
let _inst₂ := Fintype.ofEquiv G₁ e

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
⊢ ∀ (x y : G₁), e.toFun (x * y) = e.toFun x * e.toFun y
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
⊢ Set.range cs.simple = Set.range cs.simple ∪ Set.range fun i ↦ cs.simple i

Tactic:
union_self

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
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
⊢ ∀ (a : CoprodI G), a⁻¹ * a = 1

Tactic:
intro m

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
m : CoprodI G
⊢ m⁻¹ * m = 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ (lift f).range = ⨆ i, (f i).range

Tactic:
apply le_antisymm (lift_range_le _ f fun i => le_iSup (fun i => MonoidHom.range (f i)) i)
  apply iSup_le _
  rintro i _ ⟨x, rfl⟩
  exact ⟨of x, by simp only [lift_of]⟩

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

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

Tactic:
have := cs.length_mul_simple w⁻¹ i
  rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at this

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
⊢ Group.FG G

Tactic:
let f : G →* G := powMonoidHom n

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
⊢ Group.FG G
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
⊢ Function.Injective fun m ↦ mk m s

Tactic:
intro m

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m : M
⊢ ∀ ⦃a₂ : M⦄, (fun m ↦ mk m s) m = (fun m ↦ mk m s) a₂ → m = a₂
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
· rw [qsmul_of_nonpos h]
    have : a.num.natAbs • m = -a.num • m := by
      rw [← natCast_zsmul]
      congr
      simpa using h
    simp [nnqsmul_mk, this, ← neg_mk]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) → ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

pp: case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H

Tactic:
· rintro ⟨y, h_h⟩
    refine ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩
    simp only [← mul_assoc, inv_mul_cancel_right, InvMemClass.coe_inv]

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.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 : ℕ+
mc : M
sc : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • mc

Tactic:
← nsmul_le_nsmul_iff_right (show sa.val ≠ 0 by simp)

Goal state after:
case mk.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 : ℕ+
mc : M
sc : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sa • ↑sc • mb ≤ ↑sa • ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • mc
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
⊢ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * q * y

Tactic:
exact ⟨1, one_mem H, MulOpposite.unop a'⁻¹, Subgroup.mem_op.mp (by simp), by simpa
    using (eq_mul_inv_of_mul_eq ha')⟩

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Tactic:
classical
  obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
  rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
  let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
  have hf : Function.Surjective f := by
    rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]
    exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
  replace hf := card_dvd_of_surjective f hf
  rw [Nat.card_pi] at hf
  refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)
  rw [Nat.card_zpowers]
  exact Monoid.order_dvd_exponent (g : G)

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card ↥(_root_.commutator G) ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))

Tactic:
by
  have h1 := index_center_le_pow (closureCommutatorRepresentatives G)
  have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
  rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2
  rw [card_commutator_closureCommutatorRepresentatives] at h2
  replace h1 :=
    h1.trans
      (Nat.pow_le_pow_right Finite.card_pos (rank_closureCommutatorRepresentatives_le G))
  replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_left (mul_le_mul_left h1 _) 1))
  rw [← pow_succ] at h2
  refine (Nat.le_of_dvd ?_ h2).trans (Nat.pow_le_pow_left h1 _)
  exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.index_ne_zero) _

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ H.transferFocal ↑x = ↑x ^ H.index

Tactic:
transferFocal,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ (QuotientGroup.mk' H.focalSubgroupOf).transfer ↑x = ↑x ^ H.index
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_2
α : 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 ≠ []
⊢ IsReduced ((replicate n L₂).flatten ++ L₂ ++ L₃)

Tactic:
refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h

Goal state after:
case refine_2
α : 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 ≠ []
⊢ IsReduced ((replicate n L₂).flatten ++ L₂)
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₅)
⊢ reduce
      (conjugator L ++ reduceCyclically L ++ invRev (conjugator L) ++
        (conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
rw [this, ← flatten_cons, ← replicate_succ, ← isReduced_iff_reduce_eq]

Goal state after:
α : 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₅)
⊢ IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Group.IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rw [nilpotent_iff_finite_ascending_central_series]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ ⊤ ≤ upperCentralSeries G n

Tactic:
← upperCentralSeries_nilpotencyClass

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → ⊤.lowerCentralSeries n = ⊥

Tactic:
intro h
    rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]
    exact lowerCentralSeries_antitone _ h

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
⊢ I.goursatFst.prod I.goursatSnd ≤ I

Tactic:
rintro ⟨g, h⟩ ⟨hg, hh⟩

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
h : H
hg : (g, h).1 ∈ ↑I.goursatFst.toSubmonoid
hh : (g, h).2 ∈ ↑I.goursatSnd.toSubmonoid
⊢ (g, h) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ IsNilpotent G

Tactic:
use n.succ

Goal state after:
case h
G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ upperCentralSeries G n.succ = ⊤
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
⊢ IsSimpleGroup M

Tactic:
apply IsSimpleGroup.mk
  intro N nN
  cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with
  | inl h =>
    refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
    apply is_faithful.eq_of_smul_eq_smul
    intro x
    rw [one_smul]
    exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
  | inr h => exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ ↑⟨g, hg⟩ • orbit (↥H) a = orbit (↥H) a

Tactic:
← Submonoid.smul_def (S := H.toSubmonoid)

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
hg : g ∈ H
⊢ ⟨g, hg⟩ • orbit (↥H) a = orbit (↥H) a
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H✝ : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
⊢ ∀ (x : X), ∃ g, g • a = x

Tactic:
intro x; rw [← MulAction.mem_orbit_iff, H]; exact Set.mem_univ x

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α

Tactic:
rw [isPretransitive_iff_orbit_eq_univ a]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ orbit (↥N) a = Set.univ
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
h : 3 ∈ g.cycleType
⊢ (g * g).IsThreeCycle

Tactic:
obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
  simp only [mul_assoc]
  rw [hd.commute.eq, ← mul_assoc g']
  suffices hg' : orderOf g' ∣ 2 by
    rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
    exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
  rw [← lcm_cycleType, Multiset.lcm_dvd]
  intro n hn
  rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
  apply le_of_add_le_add_left
  rw [← hd.card_support_mul, h3]
  exact (c * g').support.card_le_univ

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

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

Tactic:
nontriviality α
  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]
  refine h2.antisymm ?_
  simpa [Nat.card_eq_fintype_card] using! Fintype.one_lt_card

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
hkga : k • g a = c
this : k • ⟨g, hg⟩ • a ≠ c
⊢ False

Tactic:
apply this; simp [← hkga]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ (m • embFinTwo h) 0 = c

Tactic:
e,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ (embFinTwo h') 0 = c
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ (m • embFinTwo h) 1 = d

Tactic:
e,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ (embFinTwo h') 1 = d
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
⊢ ∃ g, g • x = y

Tactic:
have hg : g ∈ stabilizer G a := by
      rw [DFunLike.ext_iff] at hgxy
      convert! hgxy (last n)
      simp [ofStabilizer.snoc_last]

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : g ∈ stabilizer G a
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := s ∩ g • s
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsPreprimitive ↥(fixingSubgroup G t) ↥(ofFixingSubgroup G t)

Tactic:
apply IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter hs_prim

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn1 : 2 * (n + 1) < Nat.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
g : G
hga : a ∈ g • s
hgb : b ∉ g • s
t : Set α := ⋯
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ s ∪ g • s ≠ ⊤
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)

Tactic:
rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]

Goal state after:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)
this :
  IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(ofFixingSubgroup G (insert a (Subtype.val '' t)))
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)
⊢ IsMultiplyPreprimitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) (n + 1 + 1)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case h
α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬AddAction.toPerm g = 1
a : α
ha : g +ᵥ a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g +ᵥ s = s
⊢ g +ᵥ a ∈ s

Tactic:
rw [← has']

Goal state after:
case h
α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬AddAction.toPerm g = 1
a : α
ha : g +ᵥ a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g +ᵥ s = s
⊢ g +ᵥ a ∈ g +ᵥ s
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
a : α
ha : g • a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g • s = s
⊢ g • a ∈ s

Tactic:
rw [← has']

Goal state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : ¬toPerm g = 1
a : α
ha : g • a ≠ a
s : ↑(powersetCard α n)
has : a ∈ s
has' : g • s = s
⊢ g • a ∈ g • s
Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs

Goal state before:
pp: M : Type u_1
G : Type u_2
H : Type u_3
inst✝² : CommMonoid M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : ⊤.LocalizationMap G
g : ⊤.LocalizationMap H
s : Submonoid G
⊢ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) = divPairs f s

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (Perm α)ᵈᵐᵃ
⊢ g ∈ stabilizer (Perm α)ᵈᵐᵃ f ↔ f ∘ ⇑(mk.symm g) = f

Tactic:
by
  simp only [MulAction.mem_stabilizer_iff]; rfl

Goal state after: