mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «0»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R
    ![(toPolygon t).vertices ((fun i ↦ i) ⟨0, ⋯⟩), (toPolygon t).vertices ((fun i ↦ i) ⟨0, ⋯⟩ + 1),
      (toPolygon t).vertices ((fun i ↦ i) ⟨0, ⋯⟩ + 2)]

Tactic:
dsimp

Goal state after:
case «0»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R
    ![(toPolygon t).vertices ((fun i ↦ i) ⟨1, ⋯⟩), (toPolygon t).vertices ((fun i ↦ i) ⟨1, ⋯⟩ + 1),
      (toPolygon t).vertices ((fun i ↦ i) ⟨1, ⋯⟩ + 2)]

Tactic:
dsimp

Goal state after:
case «1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 1, t.points 2, t.points 0]
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «2»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R
    ![(toPolygon t).vertices ((fun i ↦ i) ⟨2, ⋯⟩), (toPolygon t).vertices ((fun i ↦ i) ⟨2, ⋯⟩ + 1),
      (toPolygon t).vertices ((fun i ↦ i) ⟨2, ⋯⟩ + 2)]

Tactic:
dsimp

Goal state after:
case «2»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
h : AffineIndependent R ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 2, t.points 0, t.points 1]
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ (QuotientGroup.leftRel (H.subgroupOf K)) a b ↔
    (QuotientGroup.leftRel ((g • H).subgroupOf (g • K))) ((equivSMul g K).toEquiv a) ((equivSMul g K).toEquiv b)

Tactic:
dsimp

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ (QuotientGroup.leftRel (H.subgroupOf K)) a b ↔
    (QuotientGroup.leftRel ((g • H).subgroupOf (g • K))) ((equivSMul g K) a) ((equivSMul g K) b)
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Commensurable H

Tactic:
simp [Commensurable]

Goal state after:
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker = ⊥

Tactic:
apply bot_unique

Goal state after:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (↑(mfderiv% ⇑f.embeddingPiTangent x)).ker ≤ ⊥
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: case neg
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₁ := ⋯
_inst₂ : Fintype G₂ := ⋯
x y : G₁
hx : e x ≠ 1
hy : e y ≠ 1
hxy : e x ≠ e y
univ₂ : {e (x * y), e x, e y, 1} = univ
⊢ e x * e y = e (x * y)

Tactic:
apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _

Goal state after:
case neg
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₁ := ⋯
_inst₂ : Fintype G₂ := ⋯
x y : G₁
hx : e x ≠ 1
hy : e y ≠ 1
hxy : e x ≠ e y
univ₂ : {e (x * y), e x, e y, 1} = univ
⊢ e x * e y ∉ {e x, e y, 1}
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
⊢ False

Tactic:
by_cases h2 : n = 2

Goal state after:
case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)

Tactic:
rw [commProb_def', commProb_def', div_le_iff₀, mul_assoc, ← Nat.cast_mul, ← Subgroup.index,
    H.card_mul_index, div_mul_cancel₀, Nat.cast_le]
  · apply Nat.card_le_card_of_surjective (f := ConjClasses.map (QuotientGroup.mk' H))
    exact ConjClasses.map_surjective Quotient.mk''_surjective
  · exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'
  · exact Nat.cast_pos.mpr Finite.card_pos

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

Goal state before:
pp: n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
Nat.card_congr (oddCommuteEquiv hn),

Goal state after:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card (ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) = n * (n + 3)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

pp: case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
· rw [reciprocalFactors_even h0 h2, commProb_cons, commProb_reciprocal (n / 2),
        commProb_odd (by decide)]
    simp [field, h2.two_dvd]
    norm_num

Goal state after:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = ⊤

Tactic:
← mclosure_range_inl_union_inr,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr)
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
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ (f.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩) = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)

Tactic:
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply]
      unfold CoprodI
      rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]

Goal state after:
Module: Mathlib.Topology.VectorBundle.Riemannian

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

Tactic:
exact inv_le_of_inv_le₀ (by positivity) hδ.le

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m m' : M i
w : Word M
⊢ rcons { head := m * m' * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ } =
    rcons
      {
        head :=
          m *
            ((equivPair i)
                (rcons { head := m' * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ })).head,
        tail :=
          ((equivPair i)
              (rcons { head := m' * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯ })).tail,
        fstIdx_ne := ⋯ }

Tactic:
simp [mul_assoc, ← equivPair_symm, Equiv.apply_symm_apply]

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
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)

Tactic:
unfold IsReduced

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))
⊢ cs.length (cs.wordProd (take j ω)) = (take j ω).length ∧ cs.length (cs.wordProd (drop j ω)) = (drop j ω).length
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
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)

Tactic:
unfold IsReduced

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i').succ)) = (alternatingWord i i' (M.M i i').succ).length
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ ↑t • m ≤ ↑s • n ↔ ↑t' • m' ≤ ↑s' • n'

Tactic:
← nsmul_le_nsmul_iff_right (mul_ne_zero s'.ne_zero t'.ne_zero)

Goal state after:
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑t • m ≤ (↑s' * ↑t') • ↑s • n ↔ ↑t' • m' ≤ ↑s' • n'
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
⊢ a ∈ quotToDoubleCoset H K i ↔ mk H K a = i

Tactic:
refine ⟨fun hg ↦ by simp [mk_eq_of_doubleCoset_eq (doubleCoset_eq_of_mem hg)], fun hg ↦ ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
i : Quotient ↑H ↑K
a : G
hg : mk H K a = i
⊢ a ∈ quotToDoubleCoset H K i
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 : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ ↑(sa * sc) • (↑sb • ma + ↑sa • mb) < ↑(sa * sb) • (↑sc • ma + ↑sa • mc)

Tactic:
simp_rw [PNat.mul_coe, mul_smul, smul_add, smul_smul]

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 : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑sa * (↑sc * ↑sb)) • ma + (↑sa * (↑sc * ↑sa)) • mb < (↑sa * (↑sb * ↑sc)) • ma + (↑sa * (↑sb * ↑sa)) • mc
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hXdisj.hs
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) ((fun i ↦ X i ∪ Y i) j)

Tactic:
apply Disjoint.union_right

Goal state after:
case hXdisj.hs.ht
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (X j)

case hXdisj.hs.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (X i) (Y j)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hXdisj.ht
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) ((fun i ↦ X i ∪ Y i) j)

Tactic:
apply Disjoint.union_right

Goal state after:
case hXdisj.ht.ht
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (X j)

case hXdisj.ht.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) * ((center G).subgroupOf (_root_.commutator G)).index ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G)) * (center G).index

Tactic:
refine mul_dvd_mul ?_ h1

Goal state after:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (List.map (fun k ↦ (⇑φ)^[k] g / (⇑φ)^[k.succ] g) (List.range n)).prod = 1

Tactic:
List.prod_range_div',

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (⇑φ)^[0] g / (⇑φ)^[n] g = 1
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.commutator ↥H ≤ H.focalSubgroupOf

Tactic:
focalSubgroupOf_eq_closure

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ _root_.commutator ↥H ≤ closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}
Module: Mathlib.Order.Radical

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (Order.radical α) = Order.radical β

Tactic:
unfold Order.radical
  simp only [OrderIso.map_iInf]
  fapply Equiv.iInf_congr
  · exact f.toEquiv
  · simp

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
⊢ ⁅x, g⁆ ∈ ⊤

Tactic:
exact mem_top _

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (nilpotencyClass G) = ⊥

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (Nat.find ⋯) = ⊥
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ Nat.find ⋯ ≤ n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass ↥H ≤ nilpotencyClass G

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : G →* H
hf1 : f.ker ≤ center G
inst✝ : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ IsPretransitive G X ↔ orbit G a = Set.univ

Tactic:
rw [isPretransitive_iff_base a, Set.ext_iff]

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), ∃ g, g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ x ∈ Set.univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun g ↦ g • B

pp: case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g ↦ g • B) ∧ a ∈ b

pp: case mem_blocks
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, (B_1 ∈ range fun g ↦ g • B) → IsBlock G B_1

Tactic:
case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g

Goal state after:
case nonempty
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun g ↦ g • B

case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g ↦ g • B) ∧ a ∈ b
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 • ↑s = b • ↑s

Tactic:
← op_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
⊢ a • op c • ↑s = b • op c • ↑s
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : {a} = univ
b : X
hb : b ≠ a
⊢ b ∈ univ

Tactic:
apply Set.mem_univ

Goal state after: