mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
⊢ Nonempty (a ⟶ b) → Nonempty (Path (symgen a) (symgen b))

Tactic:
rintro ⟨p⟩

Goal state after:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ Nonempty (Path (symgen a) (symgen b))
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : (conjMap hg) ⟨x, hx⟩ = (conjMap hg) ⟨y, hy⟩
⊢ (fun x ↦ g • x) x = (fun x ↦ g • x) y

Tactic:
← SetLike.coe_eq_coe,

Goal state after:
case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : ↑((conjMap hg) ⟨x, hx⟩) = ↑((conjMap hg) ⟨y, hy⟩)
⊢ (fun x ↦ g • x) x = (fun x ↦ g • x) y
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
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : ⋂ k, ⋂ (_ : a ∈ k • A), k • A = Set.univ
⊢ B = {a}

Tactic:
· -- B = Set.univ: contradiction
    change B = Set.univ at hyp
    exfalso; apply hA'
    suffices ∃ g : G, a ∈ g • A by
      obtain ⟨g, hg⟩ := this
      have : B ⊆ g • A := Set.biInter_subset_of_mem hg
      rw [hyp, Set.univ_subset_iff, ← eq_inv_smul_iff] at this
      rw [this, Set.smul_set_univ]
    -- ∃ (g : M), a ∈ g • A
    obtain ⟨x, hx⟩ := hA
    obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G x a
    use g, x

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 α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
⊢ ∃ g, g • x = y

Tactic:
by
    let aux (x : n ↪ β) : (n ↪ α) :=
      x.trans (Function.Embedding.ofSurjective (⇑f) hf)
    have aux_apply (x : n ↪ β) (i : n) : f.toFun (aux x i) = x i := by
      simp only [trans_apply, aux]
      apply Function.surjInv_eq
    obtain ⟨g, hg⟩ := exists_smul_eq (M := G) (aux x) (aux y)
    use σ g
    ext i
    rw [DFunLike.ext_iff] at hg
    rw [smul_apply]
    simp [← aux_apply, ← hg, MulActionHom.map_smul']

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 α
m : ℕ
inst✝¹ : Finite α
p : ℕ
inst✝ : IsMultiplyPretransitive G α (m + p)
hmn : m ≤ m + p
hα : m + p ≤ Nat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
exact IsPretransitive.of_surjective_map (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_natCard hα) inferInstance

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:
← SetLike.coe_eq_coe,

Goal state after:
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⟩, ⋯⟩, ⋯⟩)
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]

Goal state after:
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⟩, ⋯⟩, ⋯⟩)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right.hφ
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⋯
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) := ⋯
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := ⋯
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
hy : y ∈ s
⊢ f (k • y) = f y

Tactic:
rw [map_smulₛₗ, hk]

Goal state after:
case right.hφ.a
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
hy : y ∈ s
⊢ f y ∈ ⇑f '' s
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case hsc_nonempty
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

Tactic:
nonempty_compl,

Goal state after:
case hsc_nonempty
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ ↑s ≠ univ
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, ⊤⁆, ⊤⁆ = ⊥

Tactic:
commutator_top_right_eq_bot_iff_le_center,

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.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x✝¹ x✝ : α × ↥s
⊢ mk x✝¹.1 x✝¹.2 ≤ mk x✝.1 x✝.2 ∨ mk x✝.1 x✝.2 ≤ mk x✝¹.1 x✝¹.2

Tactic:
simp_rw [mk_le_mk]
        exact le_total _ _

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
⊢ ∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o

Tactic:
have hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α := by
    intro l hl n hn
    apply lt_of_lt_of_le _ hc
    rw [← mem_mem_ranges_iff_lt_sum]
    exact ⟨l, hl, hn⟩

Goal state after:
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
⊢ ∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case mul
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hm : Irreducible (f (i * a))
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
rw [map_mul, irreducible_mul_iff] at hm
    obtain hia | hai := hm
    · exact ⟨a, i, hia.2, hi, mul_comm ..⟩
    · obtain ⟨u, m', hu, hm', rfl⟩ := ha hai.1
      exact ⟨u * i, m', by simpa using hu.mul hai.2, hm', by ac_rfl⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ i ∈ Finset.image f Finset.univ, (Fintype.card { a // f a = i })!

Tactic:
set φ : α → Finset.univ.image f :=
    Set.codRestrict f (Finset.univ.image f) (fun a => by simp)
  suffices ∀ g : Perm α, f ∘ g = f ↔ φ ∘ g = φ by
    simp only [this, stabilizer_card]
    apply Finset.prod_bij (fun g _ => g.val)
    · exact fun g _ => Finset.coe_mem g
    · exact fun g _ g' _ => SetCoe.ext
    · simp
    · intro i _
      apply congr_arg
      apply Fintype.card_congr
      apply Equiv.subtypeEquiv (Equiv.refl α)
      intro a
      rw [refl_apply, ← Subtype.coe_inj]
      simp only [φ, Set.val_codRestrict_apply]
  · intro g
    simp only [funext_iff]
    apply forall_congr'
    intro a
    simp only [Function.comp_apply, φ, ← Subtype.coe_inj, Set.val_codRestrict_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : a c = a d
⊢ ∃ x, ¬↑c x = x ∧ ¬↑d x = x

Tactic:
use a c

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a c) = a c
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
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ w',
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : ¬w.head = 1
w' : NormalWord d
hw' :
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := ⋯ } ∧
    List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ }.toList.head?,
        w'.head ∈ toSubgroup A B (-u)
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
exact ⟨w.head • w', by
        simpa [ReducedWord.prod, mul_assoc] using hw'⟩

Goal state after:
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
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ (comap K.subtype N).index = N.index

Tactic:
index_comap,

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ N.relIndex K.subtype.range = N.index
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId `hn₀)
     []
     [(Term.typeSpec ":" («term_≠_» `n "≠" (num "0")))]
     ":="
     (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.lia "lia" (Tactic.optConfig []))]))))))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId `aux)
     []
     [(Term.typeSpec
       ":"
       («term_=_»
        (Nat.term_! `n "!")
        "="
        («term_*_»
         (Nat.term_!
          (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) («term_-_» `n "-" (num "1")) ")")
          "!")
         "*"
         `n)))]
     ":="
     (Term.byTactic
      "by"
      (Tactic.tacticSeq
       (Tactic.tacticSeq1Indented
        [(Tactic.rwSeq
          "rw"
          (Tactic.optConfig [])
          (Tactic.rwRuleSeq
           "["
           [(Tactic.rwRule [] `mul_comm) "," (Tactic.rwRule [] (Term.app `mul_factorial_pred [`hn₀]))]
           "]")
          [])]))))))
  []
  (Tactic.rwSeq
   "rw"
   (Tactic.optConfig [])
   (Tactic.rwRuleSeq
    "["
    [(Tactic.rwRule [] `mul_comm)
     ","
     (Tactic.rwRule ["←"] (Term.app `Nat.mul_left_inj [`hn₀]))
     ","
     (Tactic.rwRule [] `mul_assoc)
     ","
     (Tactic.rwRule ["←"] `aux)
     ","
     (Tactic.rwRule
      ["←"]
      (Term.app
       `Nat.mul_left_inj
       [(Term.paren
         (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
         (Term.app `factorial_ne_zero [(Term.hole "_")])
         ")")]))
     ","
     (Tactic.rwRule [] (Term.app `Nat.choose_mul_factorial_mul_factorial [`hα]))
     ","
     (Tactic.rwRule [] `mul_assoc)]
    "]")
   [])
  []
  (Tactic.simpa
   "simpa"
   []
   []
   (Tactic.simpaArgsRest
    (Tactic.optConfig [])
    []
    []
    [(Tactic.simpArgs
      "["
      [(Tactic.simpLemma [] [] `ite_and)
       ","
       (Tactic.simpLemma [] [] (Term.app `if_pos [`hα]))
       ","
       (Tactic.simpLemma [] [] (Term.app `if_pos [`hn']))
       ","
       (Tactic.simpLemma [] [] (Term.app `mul_comm [(Term.hole "_") `n]))
       ","
       (Tactic.simpLemma [] [] `mul_assoc)]
      "]")]
    ["using"
     (Term.app
      `card_of_cycleType_mul_eq
      [`α
       (choice
        («term{_}» "{" [`n] "}")
        (Term.structInst
         "{"
         []
         (Term.structInstFields [(Term.structInstField (Term.structInstLVal `n []) [])])
         (Term.optEllipsis [])
         []
         "}"))])]))])

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
S : Sylow 2 ↥(alternatingGroup α)
⊢ ↑S = Subgroup.closure {g | (↑g).cycleType = {2, 2}}

Tactic:
← Subgroup.closure_insert_one,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ↑S = Subgroup.closure (insert 1 {g | (↑g).cycleType = {2, 2}})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
a b : α
hab : a ≠ b
⊢ swap a b ∈ ofSubtype.range

Tactic:
exact ⟨swap ⟨a, by simp⟩ ⟨b, by simp⟩, Equiv.Perm.ofSubtype_swap_eq _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z
⊢ ∀ᵐ (z : γ) ∂(η ∘ₖ κ) a, p z

Tactic:
ae_iff,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : (κ a) {a | ¬∀ᵐ (z : γ) ∂η a, p z} = 0
⊢ ((η ∘ₖ κ) a) {a | ¬p a} = 0
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((copy β ∘ₖ κ) a) (s ×ˢ t) = (κ a) (s ∩ t)

Tactic:
rw [comp_apply' _ _ _ <| hs.prod ht]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ((copy β) b) (s ×ˢ t) ∂κ a = (κ a) (s ∩ t)
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
hAbs : |1 / K| < 1
this✝ : Tendsto (fun r ↦ ↑r * ↑maxLen / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ (b : ℕ), r ≤ b → ↑b * ↑maxLen / K ^ b < 1
this : ↑(r + 1) * ↑maxLen / K ^ (r + 1) < 1
⊢ ↑(r + 1) * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ (r + 1)

Tactic:
rw [div_lt_iff₀ (by positivity)] at this

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
hAbs : |1 / K| < 1
this✝ : Tendsto (fun r ↦ ↑r * ↑maxLen / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ (b : ℕ), r ≤ b → ↑b * ↑maxLen / K ^ b < 1
this : ↑(r + 1) * ↑maxLen < 1 * K ^ (r + 1)
⊢ ↑(r + 1) * ↑(S.sup List.length) < (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ (r + 1)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ ¬IsSFiniteKernel (Kernel.prodMkLeft Unit κ)

Tactic:
rwa [Kernel.isSFiniteKernel_prodMkLeft_unit]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ (∀ (a : α), Measure.map (⇑f) (κ a) = η a) ↔ ∀ (a : α), κ a = (η.map ⇑f.symm) a

Tactic:
map_apply _ f.symm.measurable,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ (∀ (a : α), Measure.map (⇑f) (κ a) = η a) ↔ ∀ (a : α), κ a = Measure.map (⇑f.symm) (η 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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel κ.swapLeft

Tactic:
rw [Kernel.swapLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.swap ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel κ.swapLeft

Tactic:
rw [Kernel.swapLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.swap ⋯)
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel κ.swapLeft

Tactic:
rw [Kernel.swapLeft]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite (μ ⊗ₘ κ)

Tactic:
rw [compProd]; 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 α β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteMeasure (μ ⊗ₘ κ)

Tactic:
rw [compProd]; 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 α β
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsMarkovKernel κ
⊢ IsProbabilityMeasure (μ ⊗ₘ κ)

Tactic:
rw [compProd]; infer_instance

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

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun p ↦
    ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β)) p) s

Tactic:
exact Kernel.measurable_coe _ hs

Goal state after: