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

Goal state before:
pp: case mp
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
⊢ ∃ g, g • a = c ∧ g • b = d

Tactic:
obtain ⟨m, e⟩ := exists_smul_eq (M := G) (embFinTwo h) (embFinTwo h')

Goal state after:
case mp
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'
⊢ ∃ g, g • a = c ∧ g • b = d
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Surjective ⇑(conjMap_ofFixingSubgroup hst)

Tactic:
rintro ⟨x, hx⟩
    rw [eq_comm, ← inv_smul_eq_iff] at hst
    use (SubMulAction.conjMap_ofFixingSubgroup hst) ⟨x, hx⟩
    simp [← SetLike.coe_eq_coe]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
x✝¹ : ↥(fixingSubgroup M (s ∪ t))
x✝ : ↥(ofFixingSubgroup M (s ∪ t))
m : M
hm : m ∈ fixingSubgroup M (s ∪ t)
x : α
hx : x ∈ ofFixingSubgroup M (s ∪ t)
⊢ ⟨⟨↑(⟨m, hm⟩ • ⟨x, hx⟩), ⋯⟩, ⋯⟩ = ⟨⟨↑⟨m, hm⟩, ⋯⟩, ⋯⟩ • ⟨⟨↑⟨x, hx⟩, ⋯⟩, ⋯⟩

Tactic:
rw [← SetLike.coe_eq_coe, ← SetLike.coe_eq_coe]
    exact subgroup_smul_def ⟨m, hm⟩ x

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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
have h1 : sᶜ.Nonempty := nonempty_iff_ne_empty.mpr (by aesop)

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
⊢ IsCoatom (stabilizer (Perm α) s)
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ ⇑S.rightHom ∘ ⇑equiv.symm = ⇑S'.rightHom

Tactic:
MulEquiv.comp_symm_eq,

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ ⇑S.rightHom = ⇑S'.rightHom ∘ ⇑equiv.toMulEquiv
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case a
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
⊢ Nat.card α = (↑g.support).ncard + (n + 1)

Tactic:
Set.ncard_coe_finset,

Goal state after:
case a
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
⊢ Nat.card α = g.support.card + (n + 1)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hsn.a
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ Nat.card α = (↑g.support).ncard + (n + 1)

Tactic:
Set.ncard_coe_finset,

Goal state after:
case inr.hsn.a
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ Nat.card α = g.support.card + (n + 1)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 2 ≤ Subgroup.upperCentralSeries G 1

Tactic:
Subgroup.upperCentralSeries_one,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ Subgroup.upperCentralSeries G 2 ≤ center G
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ n f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤) → H.IsSubnormal

Tactic:
rintro ⟨n, hyps⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
hyps : ∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤
⊢ H.IsSubnormal
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Tactic:
rw [← comm, MonoidHom.noncommCoprod_apply]

Goal state after:
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 : mk a.1 a.2 * mk b.1 b.2 ≤ mk a.1 a.2 * mk c.1 c.2
⊢ mk b.1 b.2 ≤ mk c.1 c.2

Tactic:
by
      simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢
      exact le_of_mul_le_mul_left' hab

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h : ¬Cancels u w
⊢ Cancels (-u) (cons (↑(unitsSMulGroup φ d u w.head).1) u ((↑(unitsSMulGroup φ d u w.head).2 * w.head⁻¹) • w) ⋯ ⋯) ↔
    ¬Cancels u w

Tactic:
simpa [Cancels] using h

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
m : M
hm : Irreducible (f m)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ m = u * m'

Tactic:
induction m using WfDvdMonoid.induction_on_irreducible with

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : x ∈ Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))
⊢ Prime x

pp: case h.refine_2
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)

Tactic:
· rw [Multiset.mem_filter, Multiset.mem_map] at hx
      obtain ⟨p, hp, rfl⟩ := hx.1
      exact f.map_prime (prime_of_factor _ hp)
        (mt (fun h ↦ eq_zero_of_zero_dvd <| h ▸ map_dvd f (dvd_of_mem_factors hp)) hn) hx.2

Goal state after:
case h.refine_2
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ of g • w = g • w

Tactic:
simp +instances [instHSMul, SMul.smul, MulAction.toEndHom]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

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

Tactic:
simp +instances [instHSMul, SMul.smul, MulAction.toEndHom]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.formPerm.support.card = x.length

Tactic:
rw [List.support_formPerm_of_nodup x (hp_nodup x hx)]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.toFinset.card = x.length

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.toFinset.card = x.length

pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]

Tactic:
· -- length
        rw [List.toFinset_card_of_nodup (hp_nodup x hx)]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ σ ∈ ↑(stabilizer G T)

Tactic:
simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, mem_smul_set_iff_inv_smul_mem]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ✝ σ τ : ↥(range_toPermHom' g)
x : α
⊢ { toFun := a.ofPermHomFun (σ * τ), invFun := a.ofPermHomFun (σ * τ)⁻¹, left_inv := ⋯, right_inv := ⋯ } x =
    ({ toFun := a.ofPermHomFun σ, invFun := a.ofPermHomFun σ⁻¹, left_inv := ⋯, right_inv := ⋯ } *
        { toFun := a.ofPermHomFun τ, invFun := a.ofPermHomFun τ⁻¹, left_inv := ⋯, right_inv := ⋯ })
      x

Tactic:
by simp [mul_apply, ofPermHomFun_mul a σ τ x]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (OnCycleFactors.toPermHom g) (a.toCentralizer τ) = ↑τ

Tactic:
by
  apply ext
  intro c
  rw [OnCycleFactors.toPermHom_apply, toCentralizer_equivariant]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
⊢ con φ ≤ Con.ker (Coprod.lift (CoprodI.lift f) k)

Tactic:
by
    apply Con.conGen_le.2 fun x y => ?_
    rintro ⟨i, x', rfl, rfl⟩
    simp only [DFunLike.ext_iff, MonoidHom.coe_comp, comp_apply] at hf
    simp [hf]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ (lift f k hf) ((base φ) g) = k g

Tactic:
delta PushoutI lift base

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ ((con φ).lift (Coprod.lift (CoprodI.lift f) k) ⋯) (((con φ).mk'.comp inr) g) = k g
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
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
⊢ N ≠ ⊥

Tactic:
rintro rfl
  exact h3 ⊤ isComplement'_bot_top

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

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

Tactic:
rw [← alternatingGroup.commutator_perm_eq hα]
  have : IsPreprimitive (Perm α) (Set.powersetCard α 2) := by
    apply Set.powersetCard.isPreprimitive_perm <;> grind
  classical
  apply iwasawaStructure_two.commutator_le
  exact fixedPoints_ne_univ_of_faithfulSMul (by norm_num) (by grind)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent ↥(kleinFour α) = 1 ∨ Monoid.exponent ↥(kleinFour α) = 2
⊢ ¬Nat.card ↥(kleinFour α) ≤ 1

Tactic:
kleinFour_card_of_card_eq_four hα4

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent ↥(kleinFour α) = 1 ∨ Monoid.exponent ↥(kleinFour α) = 2
⊢ ¬4 ≤ 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∀ (x x_1 x_2 : Perm α), ⁅x_1, x_2⁆ = x → sign x = 1

Tactic:
rintro _ p q rfl

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ sign ⁅p, q⁆ = 1
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ 12 = 3 * Nat.card ↥(kleinFour α)

Tactic:
kleinFour_card_of_card_eq_four hα4

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ 12 = 3 * 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card ↥(kleinFour α) ≠ 0

Tactic:
kleinFour_card_of_card_eq_four hα4

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ 4 ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
c : Perm α
hc : (MulAut.conjNormal c) k = g
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆

Tactic:
let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
c : Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ (MulAut.conjNormal c) k ∈ ⁅⊤, ⊤⁆
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.PowSaturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

Tactic:
refine ⟨fun h n g hgn ↦ ?_, fun h n g hgn ↦ by simpa using h n g (by simpa using hgn)⟩
  obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg <;> simpa using h (by simpa using hgn)

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
⊢ ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P

Tactic:
by
  let _ := MulDistribMulAction.compHom P (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
  refine (smul_mul_inv_trivial_or_surjective hP hPK).imp (fun h ↦ ?_) fun h ↦ ?_
  · rw [eq_bot_iff, Subgroup.commutator_le]
    exact fun k hk g hg ↦ Subtype.ext_iff.mp (h ⟨g, hg⟩ ⟨k, hk⟩)
  · rw [le_antisymm_iff, Subgroup.commutator_le]
    refine ⟨fun k hk g hg ↦ P.mul_mem ((hKP hk g).mp hg) (P.inv_mem hg), fun g hg ↦ ?_⟩
    obtain ⟨k, q, hkq⟩ := h ⟨g, hg⟩
    rw [← Subtype.coe_mk g hg, ← hkq]
    exact Subgroup.commutator_mem_commutator k.2 q.2

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (copy α)

Tactic:
by rw [copy]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_left, zero_apply]
  rwa [Kernel.isSFiniteKernel_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : α → Prop
hp : MeasurableSet {x | p x}
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b).1

Tactic:
filter_upwards [h] with a ha using by simp [ha]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ + Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ) () =
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () + (Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ) ()

Tactic:
_root_.add_apply

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ + Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) () =
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () + (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()

Tactic:
_root_.add_apply

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ IsSFiniteKernel κ

Tactic:
change IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a ↦ ((), a)) (by fun_prop))

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a ↦ ((), a)) ⋯)
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 α β
f : β → γ
hf : Measurable f
⊢ (κ.map fun a ↦ (a, f a)).fst = κ

Tactic:
rw [fst_map_prod _ hf, Kernel.map_id']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst✝ : IsSFiniteKernel κ
b : β
⊢ ∫⁻ (p : α × β), f p ∂(κ ×ₖ deterministic id ⋯) b = ∫⁻ (a : α), f (a, b) ∂κ b

Tactic:
lintegral_prod_deterministic _ _ _ hf,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst✝ : IsSFiniteKernel κ
b : β
⊢ ∫⁻ (b_1 : α), f (b_1, id b) ∂κ b = ∫⁻ (a : α), f (a, b) ∂κ b
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : κ ⊗ₖ η = 0
a : α
⊢ ∫⁻ (a_1 : β), (η (a, a_1)) Set.univ ∂κ a = 0

Tactic:
rw [← setLIntegral_univ, ← Kernel.compProd_apply_prod .univ .univ, h]
      simp

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (b : Y × Z), ((Kernel.id ∥ₖ ξ) b) s ∂(κ a.1).prod (η a.2) = ((κ ∥ₖ (ξ ∘ₖ η)) a) s

Tactic:
MeasureTheory.lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable

Goal state after:
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
⊢ ∫⁻ (x : Y), ∫⁻ (y : Z), ((Kernel.id ∥ₖ ξ) (x, y)) s ∂η a.2 ∂κ a.1 = ((κ ∥ₖ (ξ ∘ₖ η)) a) s
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h : ∀ (ξ : Measure α), SFinite ξ → ξ ≪ μ → ξ ≪ ν → ξ ⊗ₘ κ ⟂ₘ ξ ⊗ₘ η
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

Tactic:
exact absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _)

Goal state after: