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

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

Tactic:
rw [this]

Goal state after:
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
h : s ⊆ t
this : s = g • s
⊢ b ∈ g • 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, ⋯⟩ • s = s

Tactic:
Submonoid.mk_smul

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.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ (S.rightHom (Function.surjInv ⋯ ((S'.rightHom.comp f) e)))⁻¹ * S.rightHom e = 1

Tactic:
rightHom_comp

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ (S.rightHom (Function.surjInv ⋯ (S.rightHom e)))⁻¹ * S.rightHom e = 1
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ ((S'.rightHom.comp f) (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * S'.rightHom e' = 1

Tactic:
rightHom_comp

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (S.rightHom (Function.surjInv ⋯ (S'.rightHom e')))⁻¹ * S'.rightHom e' = 1
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
⊢ finrank ℤ ↥A = finrank ℤ M

Tactic:
by
  refine le_antisymm A.toIntSubmodule.finrank_le ?_
  have : finrank ℤ (DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M :=
    (DistribSMul.toLinearMap ..).finrank_range_of_inj <|
      distribSMulToLinearMap_injective_of_isTorsionFree FiniteIndex.index_ne_zero
  rw [← this]
  refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_
  obtain ⟨x, rfl⟩ : ∃ x, A.index • x = m := by simpa using hm
  exact A.nsmul_index_mem x

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w w' : NormalWord d
h1 : w.head = w'.head
h2 : w.toList = w'.toList
⊢ w = w'

Tactic:
rcases w with ⟨⟨⟩, _⟩

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
d : TransversalPair G A B
w' : NormalWord d
head✝ : G
toList✝ : List (ℤˣ × G)
chain✝ : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) toList✝
mem_set✝ : ∀ (u : ℤˣ) (g : G), (u, g) ∈ { head := head✝, toList := toList✝, chain := chain✝ }.toList → g ∈ d.set u
h1 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.head = w'.head
h2 : { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ }.toList = w'.toList
⊢ { head := head✝, toList := toList✝, chain := chain✝, mem_set := mem_set✝ } = w'
Module: Mathlib.GroupTheory.IsSubnormal

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

Tactic:
rintro J ⟨F, hF, H_le, rfl, ih1⟩

Goal state after:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G},
    (∃ f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤) → H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), ((F i).subgroupOf (F (i + 1))).Normal
ih1 : F (n + 1) = ⊤
⊢ (F 0).IsSubnormal
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 : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]

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

Goal state before:
pp: case f.f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝¹ : α
b✝¹ : ↥s
a✝ : α
b✝ : ↥s
⊢ mk a✝¹ b✝¹ ≤ mk a✝ b✝ → mk a✝ b✝ ≤ mk a✝¹ b✝¹ → mk a✝¹ b✝¹ = mk a✝ b✝

Tactic:
mk_le_mk,

Goal state after:
case f.f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝¹ : α
b✝¹ : ↥s
a✝ : α
b✝ : ↥s
⊢ ↑b✝ * a✝¹ ≤ ↑b✝¹ * a✝ → ↑b✝¹ * a✝ ≤ ↑b✝ * a✝¹ → mk a✝¹ b✝¹ = mk a✝ b✝
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g✝ : G
h : Cancels u (ofGroup g✝)
⊢ ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g✝) ⋯)

Tactic:
| ofGroup =>

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
g✝ : G
hcan✝ :
  ¬Cancels (-u)
      (if h : Cancels u (ofGroup g✝) then unitsSMulWithCancel φ u (ofGroup g✝) h
      else
        let g' := unitsSMulGroup φ d u (ofGroup g✝).head;
        cons (↑g'.1) u ((↑g'.2 * (ofGroup g✝).head⁻¹) • ofGroup g✝) ⋯ ⋯)
hcan2 : Cancels u (ofGroup g✝)
hcan : ¬Cancels (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2)
⊢ cons (↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head).1) (-u)
      ((↑(unitsSMulGroup φ d (-u) (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head).2 *
          (unitsSMulWithCancel φ u (ofGroup g✝) hcan2).head⁻¹) •
        unitsSMulWithCancel φ u (ofGroup g✝) hcan2)
      ⋯ ⋯ =
    ofGroup g✝

Tactic:
| ofGroup =>

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range

Tactic:
rintro - ⟨a, rfl⟩

Goal state after:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M × N
⊢ (f.noncommCoprod g comm) a ∈ f.range ⊔ g.range
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range

Tactic:
rintro - ⟨a, rfl⟩

Goal state after:
case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ f a ∈ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
rintro - ⟨a, rfl⟩

Goal state after:
case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : N
⊢ g a ∈ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case ofGroup
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
⊢ ReducedWord.prod φ (ofGroup g✝).toReducedWord • empty = ofGroup g✝

Tactic:
| ofGroup =>

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : g.cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
| ↑g.cycleFactorsFinset

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : g.cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
| ↑(ConjAct.toConjAct k • g.cycleFactorsFinset)
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite (IteratedWreathProduct G 0)

Tactic:
rw [IteratedWreathProduct_zero]; infer_instance

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c).support
⊢ a.ofPermHomFun τ (↑c x) = ↑(↑τ c) (a.ofPermHomFun τ x)

Tactic:
· rw [notMem_support.mp hx, eq_comm, ← notMem_support,
      ofPermHomFun_apply_mem_support_cycle_iff]
    exact hx

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group (IteratedWreathProduct G 0)

Tactic:
rw [IteratedWreathProduct_zero]; infer_instance

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H

Tactic:
by
  simp_rw [residuallyFinite_iff_forall_finiteIndex, ← Classical.not_imp, ← not_forall,
    not_imp_not]

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

Goal state before:
pp: case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
rintro - ⟨a, rfl⟩

Goal state after:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : Perm ↑(Function.fixedPoints ⇑g)
⊢ ofSubtype a ∈ map (centralizer {g}).subtype (toPermHom g).ker
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 φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord d
p : Word.Pair G i := (Word.equivPair i) (CoprodI.of ((φ i) w.head) • w.toWord)
j : ι
g : G j
hg : ⟨j, g⟩ ∈ ((Word.equivPair i) w.toWord).tail.toList
⊢ g ∈ d.set j

Tactic:
exact w.normalized _ _ (Word.mem_of_mem_equivPair_tail _ hg)

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
⊢ Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3

Tactic:
rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]

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

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ Nat.card ↥(kleinFour α) ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ Function.LeftInverse
    (fun i ↦
      match i with
      | a j => Sum.inl j
      | xa j => Sum.inr j)
    fun i ↦
    match i with
    | Sum.inl j => a j
    | Sum.inr j => xa j

Tactic:
rintro (x | x)

Goal state after:
case inl
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i ↦
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inl x)) =
    Sum.inl x

case inr
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i ↦
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inr x)) =
    Sum.inr x
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ Function.RightInverse
    (fun i ↦
      match i with
      | a j => Sum.inl j
      | xa j => Sum.inr j)
    fun i ↦
    match i with
    | Sum.inl j => a j
    | Sum.inr j => xa j

Tactic:
rintro (x | x)

Goal state after:
case a
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i ↦
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (a x)) =
    a x

case xa
n : ℕ
x : ZMod (2 * n)
⊢ (fun i ↦
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i ↦
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (xa x)) =
    xa x
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a 1 ^ i.val) = 2 * n / (2 * n).gcd i.val

Tactic:
orderOf_pow,

Goal state after:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a 1) / (orderOf (a 1)).gcd i.val = 2 * n / (2 * n).gcd i.val
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((deterministic f hf) a) s = s.indicator (fun x ↦ 1) (f a)

Tactic:
rw [deterministic]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ({ toFun := fun a ↦ Measure.dirac (f a), measurable' := ⋯ } a) s = s.indicator (fun x ↦ 1) (f a)
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 α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a ↦ (Measure.comap f (κ a)) t) = fun a ↦ (κ a) (f '' t)
⊢ Measurable fun b ↦ (Measure.comap f (κ b)) t

Tactic:
rw [this]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this : (fun a ↦ (Measure.comap f (κ a)) t) = fun a ↦ (κ a) (f '' t)
⊢ Measurable fun a ↦ (κ a) (f '' t)
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this : (fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)

Tactic:
rw [this]

Goal state after:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this : (fun a ↦ (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a ↦ (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
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 η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  (fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)) = fun y ↦
    ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
⊢ Measurable fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)

Tactic:
rw [this]

Goal state after:
α : 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 η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  (fun y ↦ ((prodMkLeft α η) y.1) (Prod.mk y.2 ⁻¹' s)) = fun y ↦
    ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
⊢ Measurable fun y ↦ ((prodMkRight β (prodMkLeft α η)) y) (Prod.mk y.2 ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
have := IsMarkovKernel.comap κ hg

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
this : IsMarkovKernel (κ.comap g hg)
⊢ IsZeroOrMarkovKernel (κ.comap g hg)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
f : δ → β
hf : Measurable f
⊢ (κ.sectR a).comap f hf = κ.comap (fun d ↦ (a, f d)) ⋯

Tactic:
ext d s
  rw [comap_apply, sectR_apply, comap_apply]

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

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x = 0

Tactic:
suffices ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 0 by
      rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]

Goal state after:
case e'_2.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) = 0
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α δ
inst✝ : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
⊢ (κ.map f ×ₖ η.map g) x = ((κ ×ₖ η).map (Prod.map f g)) x

Tactic:
rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]

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

Goal state before:
pp: 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 ξ
this : swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ)
⊢ swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∘ₖ η ∥ₖ κ))

Tactic:
rw [this]

Goal state after: