mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * a k = a i * (a j * a k)

pp: case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * xa k = a i * (a j * xa k)

pp: case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * a k = a i * (xa j * a k)

pp: case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * xa k = a i * (xa j * xa k)

pp: case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * a k = xa i * (a j * a k)

pp: case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * xa k = xa i * (a j * xa k)

pp: case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * a k = xa i * (xa j * a k)

pp: case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * xa k = xa i * (xa j * xa k)

Tactic:
<;>

Goal state after:
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * a k = a i * (a j * a k)

case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * xa k = a i * (a j * xa k)

case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * a k = a i * (xa j * a k)

case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * xa k = a i * (xa j * xa k)

case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * a k = xa i * (a j * a k)

case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * xa k = xa i * (a j * xa k)

case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * a k = xa i * (xa j * a k)

case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * xa k = xa i * (xa j * xa k)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (i + j + k) = a (i + (j + k))

pp: case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (i + j)) = xa (k - j - i)

pp: case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (j - i + k) = xa (j + k - i)

pp: case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (j - i)) = a (i + (↑n + k - j))

pp: case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (i + j + k) = xa (i + (j + k))

pp: case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (i + j)) = a (↑n + (k - j) - i)

pp: case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + j - i + k) = a (↑n + (j + k) - i)

pp: case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (↑n + j - i)) = xa (i + (↑n + k - j))

Tactic:
<;>

Goal state after:
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (i + j + k) = a (i + (j + k))

case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (i + j)) = xa (k - j - i)

case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (j - i + k) = xa (j + k - i)

case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (j - i)) = a (i + (↑n + k - j))

case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (i + j + k) = xa (i + (j + k))

case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (i + j)) = a (↑n + (k - j) - i)

case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + j - i + k) = a (↑n + (j + k) - i)

case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (↑n + j - i)) = xa (i + (↑n + k - j))
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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: 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

pp: 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

Tactic:
<;>

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: case a
n : ℕ
k : ZMod (2 * 0)
⊢ (fun x ↦
        match x with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun x ↦
          match x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (a k)) =
    a k

pp: case xa
n : ℕ
k : ZMod (2 * 0)
⊢ (fun x ↦
        match x with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun x ↦
          match x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (xa k)) =
    xa k

Tactic:
<;>

Goal state after:
case a
n : ℕ
k : ZMod (2 * 0)
⊢ (fun x ↦
        match x with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun x ↦
          match x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (a k)) =
    a k

case xa
n : ℕ
k : ZMod (2 * 0)
⊢ (fun x ↦
        match x with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun x ↦
          match x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (xa k)) =
    xa k
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case r
n : ℕ
k : ZMod 0
⊢ (fun x ↦
        match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun x ↦
          match x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.r k)) =
    DihedralGroup.r k

pp: case sr
n : ℕ
k : ZMod 0
⊢ (fun x ↦
        match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun x ↦
          match x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.sr k)) =
    DihedralGroup.sr k

Tactic:
<;>

Goal state after:
case r
n : ℕ
k : ZMod 0
⊢ (fun x ↦
        match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun x ↦
          match x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.r k)) =
    DihedralGroup.r k

case sr
n : ℕ
k : ZMod 0
⊢ (fun x ↦
        match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun x ↦
          match x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.sr k)) =
    DihedralGroup.sr k
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case a.a
n : ℕ
k l : ZMod (2 * 0)
⊢ (match a k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match a k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match a l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

pp: case a.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ (match a k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match a k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match xa l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

pp: case xa.a
n : ℕ
k l : ZMod (2 * 0)
⊢ (match xa k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match xa k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match a l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

pp: case xa.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ (match xa k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match xa k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match xa l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

Tactic:
<;>

Goal state after:
case a.a
n : ℕ
k l : ZMod (2 * 0)
⊢ (match a k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match a k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match a l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

case a.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ (match a k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match a k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match xa l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

case xa.a
n : ℕ
k l : ZMod (2 * 0)
⊢ (match xa k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match xa k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match a l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

case xa.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ (match xa k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match xa k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match xa l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ ↑n = 0 ∨ g ∈ H

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ -↑n = 0 ∨ g ∈ H

Tactic:
<;>

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ ↑n = 0 ∨ g ∈ H

case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ -↑n = 0 ∨ g ∈ H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑g).support ⊆ ↑⟨(↑g).support, ⋯⟩ ∧ (↑g = 1 ∨ (↑g).cycleType = {2, 2})

pp: case hs
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑⟨(↑g).support, ⋯⟩).card = 4

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑g).support ⊆ ↑⟨(↑g).support, ⋯⟩ ∧ (↑g = 1 ∨ (↑g).cycleType = {2, 2})

case hs
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
⊢ (↑⟨(↑g).support, ⋯⟩).card = 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case hn
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ 4 < Nat.card α

pp: case hα
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 4

Tactic:
<;>

Goal state after:
case hn
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ 4 < Nat.card α

case hα
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ Nat.card α ≠ 2 * 4
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: ⊢ normalClosure {⟨finRotate 5, ⋯⟩} = ⊤

Tactic:
have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)

Goal state after:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
⊢ normalClosure {⟨finRotate 5, ⋯⟩} = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: ⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Tactic:
have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)

Goal state after:
this : IsSimpleGroup ↥(alternatingGroup (Fin 5))
⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤
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)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
⊢ w = Word.empty

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩
  rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩
  rcases h with ⟨h, heq⟩
  have : (NormalWord.prod (d := d) ⟨.empty, h, by simp⟩) = base φ h := by
    simp [NormalWord.prod]
  rw [← hw'prod, ← this] at heq
  suffices w'.toWord = .empty by
    simp [this, @eq_comm _ []] at hw'map
    ext
    simp [hw'map]
  rw [← prod_injective heq]

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

Goal state before:
pp: case refine_2
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)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = ⟨g, hg⟩
⊢ ↑(k • q * q⁻¹) ∈ ⁅K, P⁆

Tactic:
exact Subgroup.commutator_mem_commutator k.2 q.2

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P → ¬p ∣ Nat.card ↥(commutator G)

pp: case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ↑P ≤ commutator G → ¬p ∣ (commutator G).index

Tactic:
<;>

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P → ¬p ∣ Nat.card ↥(commutator G)

case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ ↑P ≤ commutator G → ¬p ∣ (commutator G).index
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
h✝ : Nonempty α
inst✝ : IsZeroOrMarkovKernel 0
⊢ bound 0 ≤ 1

pp: case inr.inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
h✝¹ : Nonempty α
h✝ : IsMarkovKernel κ
⊢ κ.bound ≤ 1

Tactic:
<;>

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
h✝ : Nonempty α
inst✝ : IsZeroOrMarkovKernel 0
⊢ bound 0 ≤ 1

case inr.inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
h✝¹ : Nonempty α
h✝ : IsMarkovKernel κ
⊢ κ.bound ≤ 1
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ swap hammingDist = hammingDist

Tactic:
funext x y

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : i = 0
⊢ (κ a) s = (κ a) s

pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : ¬i = 0
⊢ (0 a) s = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : i = 0
⊢ (κ a) s = (κ a) s

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h✝ : ¬i = 0
⊢ (0 a) s = 0
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
h✝ : a ∈ s
⊢ (κ a) t = (κ a) t

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
h✝ : a ∉ s
⊢ (η a) t = (η a) t

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
h✝ : a ∈ s
⊢ (κ a) t = (κ a) t

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
h✝ : a ∉ s
⊢ (η a) t = (η a) t
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∈ s
⊢ κ a = Measure.sum fun n ↦ (κ.seq n) a

pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∉ s
⊢ η a = Measure.sum fun n ↦ (η.seq n) a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∈ s
⊢ κ a = Measure.sum fun n ↦ (κ.seq n) a

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
h✝ : a ∉ s
⊢ η a = Measure.sum fun n ↦ (η.seq n) a
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
h✝ : a ∈ s
⊢ ∫⁻ (b : β), g b ∂κ a = ∫⁻ (b : β), g b ∂κ a

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
h✝ : a ∉ s
⊢ ∫⁻ (b : β), g b ∂η a = ∫⁻ (b : β), g b ∂η a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
h✝ : a ∈ s
⊢ ∫⁻ (b : β), g b ∂κ a = ∫⁻ (b : β), g b ∂κ a

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
h✝ : a ∉ s
⊢ ∫⁻ (b : β), g b ∂η a = ∫⁻ (b : β), g b ∂η a
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
h✝ : a ∈ s
⊢ ∫⁻ (b : β) in t, g b ∂κ a = ∫⁻ (b : β) in t, g b ∂κ a

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
h✝ : a ∉ s
⊢ ∫⁻ (b : β) in t, g b ∂η a = ∫⁻ (b : β) in t, g b ∂η a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
h✝ : a ∈ s
⊢ ∫⁻ (b : β) in t, g b ∂κ a = ∫⁻ (b : β) in t, g b ∂κ a

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
h✝ : a ∉ s
⊢ ∫⁻ (b : β) in t, g b ∂η a = ∫⁻ (b : β) in t, g b ∂η a
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 γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)

Tactic:
refine ext_fun fun a f hf => ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a