awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
h2 : ¬Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))

Tactic:
ring
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ring
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
h2 : ¬Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a ⋯ b h2 : (a : γ) → ℝ≥0∞) c : ℝ≥0∞)) =
    HMul.hMul (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a h1 b ⋯ : (a : γ) → ℝ≥0∞) c : ℝ≥0∞))

Tactic:
ring
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
simp :
  Eq (α := ℝ≥0∞) (∑' (x : β), s.indicator (⇑(p.bindOnSupport f) : (a : β) → ℝ≥0∞) x)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
          else ∑' (x : β), s.indicator (⇑(f a ⋯) : (a : β) → ℝ≥0∞) x :
          ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) (((p.bindOnSupport f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
            else ((f a h).toOuterMeasure : (a : Set β) → ℝ≥0∞) s :
            ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
simp only [toOuterMeasure_apply]

Premises used: PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
pos :
  ∀ (hbs : b ∈ s),
    Eq (α := ℝ≥0∞)
      (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞))
      (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞))
neg : ∀ (hbs : b ∉ s), Eq (α := ℝ≥0∞) 0 (∑' (a : α), 0)
⊢ Eq (α := ℝ≥0∞)
    (if b ∈ s then
      ∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
    else 0)
    (∑' (a : α),
      if b ∈ s then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
      else 0)

Tactic:
split_ifs with hbs
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
hbs : b ∈ s
⊢ Eq (α := ℝ≥0∞)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
          ℝ≥0∞))
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
          ℝ≥0∞))

Tactic:
simp only [tsum_zero]

Premises used: tsum_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
hbs : b ∉ s
⊢ Eq (α := ℝ≥0∞) 0 (∑' (a : α), 0)

Tactic:
simp only [tsum_zero]

Premises used: tsum_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : β) (a : α),
      if b ∈ s then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
      else 0)
    (∑' (a : α) (b : β),
      if b ∈ s then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
      else 0)

Tactic:
ENNReal.tsum_comm

Premises used: ENNReal.tsum_comm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
⊢ (∑' (b : β),
      if b ∈ s then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞)
      else 0) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β),
          if b ∈ s then
            if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b
          else 0 :
        ℝ≥0∞)

Tactic:
simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero]

Premises used: ENNReal.tsum_mul_left, mul_ite, MulZeroClass.mul_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
pos :
  ∀ (ha : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (b : β), if b ∈ s then 0 else 0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (ha : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (b : β), if b ∈ s then (f a ha : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (b : β), if b ∈ s then (f a ha : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β),
          if b ∈ s then
            if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b
          else 0 :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else ∑' (b : β), if b ∈ s then (f a h : (a : β) → ℝ≥0∞) b else 0 :
        ℝ≥0∞)

Tactic:
split_ifs with ha
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (b : β), if b ∈ s then 0 else 0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [ite_self, tsum_zero]

Premises used: ite_self, tsum_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β), if b ∈ s then (f a ha : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β), if b ∈ s then (f a ha : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)

Tactic:
simp only [ite_self, tsum_zero]

Premises used: ite_self, tsum_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ Eq (α := ℝ≥0∞) (∑' (x : β), s.indicator (⇑(p.bindOnSupport f) : (a : β) → ℝ≥0∞) x)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
          else ∑' (x : β), s.indicator (⇑(f a ⋯) : (a : β) → ℝ≥0∞) x :
          ℝ≥0∞))

Tactic:
calc
    (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
        ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      tsum_congr fun b => by split_ifs with hbs <;> simp only [tsum_zero]
    _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
    _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
      tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero]

Premises used: HMul.hMul, tsum_congr, Membership.mem, dite, tsum, ENNReal.tsum_comm, OfNat.ofNat, Eq, DFunLike.coe, SummationFilter.unconditional, ite
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ Eq (α := ℝ≥0∞) (∑' (x : β), s.indicator (⇑(p.bindOnSupport f) : (a : β) → ℝ≥0∞) x)
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
          else ∑' (x : β), s.indicator (⇑(f a ⋯) : (a : β) → ℝ≥0∞) x :
          ℝ≥0∞))

Tactic:
classical
  calc
    (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
        ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      tsum_congr fun b => by split_ifs with hbs <;> simp only [tsum_zero]
    _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
    _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
      tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero]

Premises used: tsum_congr, ENNReal.tsum_comm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
inst : MeasurableSpace β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((p.bindOnSupport f).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
            else (((f a h).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s :
            ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
simp only [toMeasure_apply_eq_toOuterMeasure_apply _ hs, toOuterMeasure_bindOnSupport_apply]

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_bindOnSupport_apply
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
u v : (i : ι) → Ω → β i
inst_2 : (i : ι) → Mul (β i)
inst_3 : ∀ (i : ι), MeasurableMul₂.{u_3} (β i)
hu : Adapted (β := β) f u
hv : Adapted (β := β) f v
⊢ Adapted (β := β) f (u * v)

Tactic:
fun i => (hu i).mul (hv i)

Premises used: Measurable.mul, MeasureTheory.Adapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
u v : (i : ι) → Ω → β i
inst_2 : (i : ι) → Div (β i)
inst_3 : ∀ (i : ι), MeasurableDiv₂.{u_3} (β i)
hu : Adapted (β := β) f u
hv : Adapted (β := β) f v
⊢ Adapted (β := β) f (u / v)

Tactic:
fun i => (hu i).div (hv i)

Premises used: Measurable.div, MeasureTheory.Adapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : (i : ι) → Group (β i)
inst_3 : ∀ (i : ι), MeasurableInv.{u_3} (β i)
hu : Adapted (β := β) f u
⊢ Adapted (β := β) f u⁻¹

Tactic:
fun i => (hu i).inv

Premises used: MeasureTheory.Adapted, Measurable.inv
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
𝕂 : Type u_4
inst_2 : MeasurableSpace 𝕂
inst_3 : (i : ι) → SMul.{u_4, u_3} 𝕂 (β i)
inst_4 : ∀ (i : ι), MeasurableSMul.{u_4, u_3} 𝕂 (β i)
c : 𝕂
hu : Adapted (β := β) f u
⊢ Adapted (β := β) f (c • u)

Tactic:
fun i => (hu i).const_smul c

Premises used: Measurable.const_smul, MeasureTheory.Adapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
i : ι
hf : Adapted (β := β) f u
⊢ inst_1 i ≤ inst_1 i

Tactic:
rfl
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
i j : ι
hf : Adapted (β := β) f u
hij : i ≤ j
⊢ inst_1 i ≤ inst_1 i

Tactic:
rfl
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → MeasurableSpace (β i)
f : Filtration ι m
x : (i : ι) → β i
⊢ Adapted (β := β) f fun (i : ι) (x_1 : Ω) ↦ x i

Tactic:
fun _ ↦ measurable_const

Premises used: MeasureTheory.Adapted, measurable_const
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : Type u_4
inst_1 : MeasurableSpace β
f : Filtration ι m
x : β
⊢ Adapted (β := fun (x : ι) ↦ β) f fun (x_1 : ι) (x_2 : Ω) ↦ x

Tactic:
adapted_const' _ _

Premises used: MeasureTheory.adapted_const'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u v : (i : ι) → Ω → β i
inst_2 : (i : ι) → Mul (β i)
inst_3 : ∀ (i : ι), ContinuousMul.{u_3} (β i)
hu : StronglyAdapted (β := β) f u
hv : StronglyAdapted (β := β) f v
⊢ StronglyAdapted (β := β) f (u * v)

Tactic:
fun i => (hu i).mul (hv i)

Premises used: MeasureTheory.StronglyMeasurable.mul, MeasureTheory.StronglyAdapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u v : (i : ι) → Ω → β i
inst_2 : (i : ι) → Div (β i)
inst_3 : ∀ (i : ι), ContinuousDiv.{u_3} (β i)
hu : StronglyAdapted (β := β) f u
hv : StronglyAdapted (β := β) f v
⊢ StronglyAdapted (β := β) f (u / v)

Tactic:
fun i => (hu i).div' (hv i)

Premises used: MeasureTheory.StronglyAdapted, MeasureTheory.StronglyMeasurable.div'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : (i : ι) → Group (β i)
inst_3 : ∀ (i : ι), ContinuousInv.{u_3} (β i)
hu : StronglyAdapted (β := β) f u
⊢ StronglyAdapted (β := β) f u⁻¹

Tactic:
fun i => (hu i).inv

Premises used: MeasureTheory.StronglyMeasurable.inv, MeasureTheory.StronglyAdapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : (i : ι) → SMul ℝ (β i)
inst_3 : ∀ (i : ι), ContinuousConstSMul.{0, u_3} ℝ (β i)
c : ℝ
hu : StronglyAdapted (β := β) f u
⊢ StronglyAdapted (β := β) f (c • u)

Tactic:
fun i => (hu i).const_smul c

Premises used: MeasureTheory.StronglyAdapted, MeasureTheory.StronglyMeasurable.const_smul
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_4
u : (i : ι) → Ω → β i
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
hu : StronglyAdapted (β := β) f u
⊢ StronglyAdapted (β := fun (t : ι) ↦ ℝ) f fun (t : ι) (ω : Ω) ↦ ‖u t ω‖

Tactic:
fun t ↦ (hu t).norm

Premises used: MeasureTheory.StronglyAdapted, MeasureTheory.StronglyMeasurable.norm
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
i : ι
hf : StronglyAdapted (β := β) f u
⊢ StronglyMeasurable (u i)

Tactic:
(hf i).mono (f.le i)

Premises used: MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
i j : ι
hf : StronglyAdapted (β := β) f u
hij : i ≤ j
⊢ StronglyMeasurable (u i)

Tactic:
(hf i).mono (f.mono hij)

Premises used: MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
mΒ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : ∀ (i : ι), PseudoMetrizableSpace.{u_3} (β i)
hf : StronglyAdapted (β := β) f u
⊢ Adapted (β := β) f u

Tactic:
fun _ ↦ (hf _).measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Adapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
mΒ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), OpensMeasurableSpace.{u_3} (β i)
inst_3 : ∀ (i : ι), PseudoMetrizableSpace.{u_3} (β i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_3} (β i)
hf : Adapted (β := β) f u
⊢ StronglyAdapted (β := β) f u

Tactic:
fun _ ↦ (hf _).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyAdapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
f : Filtration ι m
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
mΒ : (i : ι) → MeasurableSpace (β i)
inst_2 : ∀ (i : ι), BorelSpace.{u_3} (β i)
inst_3 : ∀ (i : ι), PseudoMetrizableSpace.{u_3} (β i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_3} (β i)
⊢ StronglyAdapted (β := β) f u ↔ Adapted (β := β) f u

Tactic:
⟨fun h ↦ h.adapted, fun h ↦ h.stronglyAdapted⟩

Premises used: MeasureTheory.StronglyAdapted.adapted, Iff.intro, MeasureTheory.Adapted.stronglyAdapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
f : Filtration ι m
x : (i : ι) → β i
⊢ StronglyAdapted (β := β) f fun (i : ι) (x_1 : Ω) ↦ x i

Tactic:
fun _ ↦ stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyAdapted
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : Type u_4
inst_1 : TopologicalSpace β
f : Filtration ι m
x : β
⊢ StronglyAdapted (β := fun (x : ι) ↦ β) f fun (x_1 : ι) (x_2 : Ω) ↦ x

Tactic:
stronglyAdapted_const' _ _

Premises used: MeasureTheory.stronglyAdapted_const'
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
inst_2 : (i : ι) → Zero (β i)
f : Filtration ι m
⊢ StronglyAdapted (β := β) f 0

Tactic:
fun i ↦ @stronglyMeasurable_zero Ω (β i) (f i) _ _

Premises used: MeasureTheory.StronglyAdapted, MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : Type u_4
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : Filtration ι m
⊢ StronglyAdapted (β := fun (a : ι) ↦ β) f 0

Tactic:
fun i ↦ @stronglyMeasurable_zero Ω β (f i) _ _

Premises used: MeasureTheory.StronglyAdapted, MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)

Tactic:
StronglyMeasurable.mono ?_ (le_iSup₂_of_le i (le_refl i) le_rfl)

Premises used: le_refl, le_rfl, MeasureTheory.StronglyMeasurable.mono, le_iSup₂_of_le
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
refine : StronglyMeasurable (u i)
⊢ StronglyMeasurable (u i)

Tactic:
refine StronglyMeasurable.mono ?_ (le_iSup₂_of_le i (le_refl i) le_rfl)

Premises used: le_refl, le_rfl, MeasureTheory.StronglyMeasurable.mono, le_iSup₂_of_le
-- Module: Mathlib.Probability.Process.Adapted
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst : Preorder ι
β : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst_2 : ∀ (i : ι), MetrizableSpace.{u_3} (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst_3 : ∀ (i : ι), BorelSpace.{u_3} (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
rw : Measurable (u i) ∧ IsSeparable (Set.range (u i))
⊢ StronglyMeasurable (u i)

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Premises used: stronglyMeasurable_iff_measurable_separable