mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∈ stabilizer G (orbit (↥H) a)

Tactic:
mem_stabilizer_iff,

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 • orbit (↥H) a = orbit (↥H) a
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
hn : ↑m + ↑n ≤ ENat.card α
x : Fin m ↪ α
⊢ ↑(range ⇑x).ncard + ↑?m.23 ≤ ENat.card α

Tactic:
by simpa [← Nat.card_coe_set_eq, Nat.card_range_of_injective x.injective]

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

Goal state before:
pp: case mpr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
x : α
⊢ x = a ∨ x ∈ Subtype.val '' t → x ∈ s'

Tactic:
rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)

Goal state after:
case mpr.inl
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
s' : Set α := g • s
hs' : s' = g • s
x : α
H : IsMultiplyPreprimitive (↥(stabilizer M x)) (↥(ofStabilizer M x)) n
hg : g • b = x
t : Set ↥(ofStabilizer M x) := Subtype.val ⁻¹' s'
⊢ x ∈ s'

case mpr.inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
y : ↥(ofStabilizer M a)
hy : y ∈ t
⊢ ↑y ∈ s'
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := ⋯
k : Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := ⋯
x' : Fin (Fintype.card α - 1) ↪ α := ⋯
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Bijective x.toFun

Tactic:
Fintype.bijective_iff_injective_and_card

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x✝ : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j.trans x✝
g : ↥G
hg' : g • x' = k • x'
x : Fin (Fintype.card α) ↪ α
⊢ Function.Injective x.toFun ∧ Fintype.card (Fin (Fintype.card α)) = Fintype.card α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ s ∨ x ∉ g • s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩

Tactic:
rcases hx with hx | hx

Goal state after:
case inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩

case inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ ⟨Perm.ofSubtype g, ⋯⟩ ∈ stabilizer (↥(alternatingGroup α)) s

Tactic:
mem_stabilizer_iff,

Goal state after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ ⟨Perm.ofSubtype g, ⋯⟩ • s = s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ ⟨Perm.ofSubtype g, ⋯⟩ ∈ stabilizer (↥(alternatingGroup α)) s

pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ toPerm ⟨⟨Perm.ofSubtype g, ⋯⟩, ?property✝⟩ = g

Tactic:
· rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ toPerm ⟨⟨Perm.ofSubtype g, ⋯⟩, ⋯⟩ = g
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
⊢ ⟨Perm.ofSubtype g * k, ⋯⟩ ∈ stabilizer (↥(alternatingGroup α)) s

Tactic:
mem_stabilizer_iff,

Goal state after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
⊢ ⟨Perm.ofSubtype g * k, ⋯⟩ • s = s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
hG : stabilizer (↥G) s = ⊤
this : G = Subgroup.map G.subtype ⊤
⊢ G ≤ stabilizer M s

Tactic:
rw [this, Subgroup.map_le_iff_le_comap]

Goal state after:
case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
hG : stabilizer (↥G) s = ⊤
this : G = Subgroup.map G.subtype ⊤
⊢ ⊤ ≤ Subgroup.comap G.subtype (stabilizer M s)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
hf : Function.Surjective ⇑f
⊢ IsPerfect G'

Tactic:
← top_iff,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsPerfect G
hf : Function.Surjective ⇑f
⊢ IsPerfect ↥⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
⊢ ⊤.IsSubnormal

pp: case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
· exact top

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal
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:
mem_stabilizer_iff,

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
⊢ σ • T = T
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
⊢ ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T

Tactic:
exact fun a ↦ ⟨fun h ↦ smul_inv_smul σ a ▸ key0 σ hσ (σ⁻¹ • a) h, key0 σ⁻¹ (hS σ hσ) a⟩

Goal state after:
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
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α := (fixedBy α f)ᶜ
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S

Tactic:
clear_value supp

Goal state after:
case refine_2
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp : Set α
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
  suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_ofPred, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
  simp only [Fintype.card_eq_nat_card]
  congr
  ext
  rw [mem_range_toPermHom_iff', Set.mem_ofPred_eq]

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 : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i : ι
h : __src✝.fstIdx = some i
⊢ False

Tactic:
by cases h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ (if Even (m.sum + m.card) then #{g | g.cycleType = m} else 0) = 0

Tactic:
split_ifs with hm'

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ #{g | g.cycleType = m} = 0

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : ¬Even (m.sum + m.card)
⊢ 0 = 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
⊢ a.toCentralizer ⟨τ, hτ⟩ ^ 2 = 1

Tactic:
← map_pow

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
⊢ a.toCentralizer (⟨τ, hτ⟩ ^ 2) = 1
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:
by
  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: case inl
α : 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
hk22 : (↑k).cycleType = {2, 2}
⊢ 1 ∈ commutator ↥(alternatingGroup α)

Tactic:
exact Subgroup.one_mem _

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

Goal state before:
pp: n : ℕ
i : ZMod (2 * n)
⊢ a (↑n + ↑n) = a ↑(2 * n)

Tactic:
by simp [Nat.cast_add, two_mul]

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
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
⊢ (↑k).cycleType = {2, 2}

Tactic:
have hk2 := comm_le hk

Goal state after:
α : 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
hk2 : k ∈ kleinFour α
⊢ (↑k).cycleType = {2, 2}
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P

Tactic:
obtain ⟨k, hk⟩ := P.2.exists_card_eq

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
k : ℕ
hk : Nat.card ↥↑P = p ^ k
⊢ IsCyclic ↥↑P
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
hφ : ∀ (i : ι), Injective ⇑(φ i)
d : Transversal φ
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : (i : ι) → DecidableEq (G i) := fun i ↦ Classical.decEq (G i)
a₁✝ a₂✝ : H
h : ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₁✝ = ((fun x1 x2 ↦ x1 • x2) ∘ ⇑(base φ)) a₂✝
w : NormalWord d
⊢ a₁✝ • w = a₂✝ • w

Tactic:
simp_all [funext_iff, base_smul_eq_smul]

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

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

Tactic:
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.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) s = ((Kernel.sum fun n ↦ if n = 0 then κ else 0) a) s

Tactic:
Kernel.sum_apply' _ _ hs

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) s = ∑' (n : ℕ), ((if n = 0 then κ else 0) a) s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel Kernel.id

Tactic:
Kernel.id

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic id ⋯)
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n ↦ (κs (e n).1).seq (e n).2) a) s

Tactic:
Kernel.sum_apply' _ _ hs

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι) (n_1 : ℕ), (((κs n).seq n_1) a) s = ∑' (n : ℕ), (((κs (e n).1).seq (e n).2) a) s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
⊢ Measurable fun a ↦ (κ a).restrict s

Tactic:
refine Measure.measurable_of_measurable_coe _ fun t ht => ?_
    simp_rw [Measure.restrict_apply ht]
    exact Kernel.measurable_coe κ (ht.inter hs)

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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ (Measure.sum fun n ↦ Measure.comap f ((κ.seq n) a)) t = (Measure.sum fun n ↦ (κ.seq n) a) (f '' t)

Tactic:
Measure.sum_apply _ ht,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ ∑' (i : ℕ), (Measure.comap f ((κ.seq i) a)) t = (Measure.sum fun n ↦ (κ.seq n) a) (f '' t)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image concatFn Finset.univ
w✝ : Fin r → ↥S
left✝ : w✝ ∈ Finset.univ
hx : concatFn w✝ ∈ T
⊢ (concatFn w✝).length ∈ Finset.Icc r (r * maxLen)

Tactic:
exact concatFn_length_mem_Icc
      (fun c hnil => h.epsilon_not_mem (by simpa [hnil] using c.prop))

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 1 / K < 1

Tactic:
div_lt_one

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 1 < K

α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : 1 < ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
K : ℝ := ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length
maxLen : ℕ := S.sup List.length
⊢ 0 < K
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ✝ : Kernel α β
η✝ : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
⊢ Measurable fun x ↦ (κ x.1).prod (η x.2)

Tactic:
by
      have hκ := h.1
      have hη := h.2
      refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
      simp_rw [Measure.prod_apply hs]
      refine Measurable.lintegral_kernel_prod_right'
        (f := fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s)) (κ := prodMkRight γ κ) ?_
      have : (fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s))
          = fun y ↦ prodMkRight β (prodMkLeft α η) y (Prod.mk y.2 ⁻¹' s) := rfl
      rw [this]
      exact measurable_kernel_prodMk_left (measurable_fst.snd.prodMk measurable_snd hs)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
hf : Measurable f
⊢ ((map 0 f) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [map_apply, hf]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Kernel.id a) (Prod.mk a ⁻¹' s) ∂μ = μ (Function.diag ⁻¹' s)

Tactic:
simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = μ (Function.diag ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((deterministic f hf) b) s ∂κ a = (κ a) (f ⁻¹' s)

Tactic:
deterministic_apply' hf _ hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
hf : Measurable f
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun x ↦ 1) (f b) ∂κ a = (κ a) (f ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ deterministic id ⋯ = Kernel.id

Tactic:
Kernel.id

Goal state after: