awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
refine_1 :
  ∀ (t : Set ι),
    (∃ (x : ι), Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} x) → ∃ (a : ι), ∀ b ≤ a, b ∉ t
⊢ ∀ (t : Set ι), BddBelow t → Membership.mem (γ := Filter ι) atBot tᶜ

Tactic:
simp only [mem_atBot_sets, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]

Premises used: lowerBounds, Set.Nonempty, BddBelow, Filter.mem_atBot_sets, Set.mem_compl_iff
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
⊢ ∃ (b : ι), b < a

Tactic:
exists_lt a

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
refine_1 : ∀ (b : ι) (hb : b < a), ∃ (a : ι), ∀ b ≤ a, b ∉ t
⊢ ∃ (a : ι), ∀ b ≤ a, b ∉ t

Tactic:
obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
⊢ ∃ (a : ι), ∀ b ≤ a, b ∉ t

Tactic:
⟨b, fun c hc hct => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
refine_1 : ∀ (c : ι) (hc : c ≤ b) (hct : c ∈ t), False
⊢ ∃ (a : ι), ∀ b ≤ a, b ∉ t

Tactic:
refine ⟨b, fun c hc hct => ?_⟩
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
refine_1 : ∀ i ∈ t, c < i
⊢ False

Tactic:
suffices ∀ i ∈ t, c < i from lt_irrefl c (this c hct)
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ i ∈ t, c < i

Tactic:
fun i hi => hc.trans_lt (hb.trans_le (ha hi))

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : Membership.mem (γ := Set ι) {x : ι | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a} a
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ i ∈ t, c < i

Tactic:
exact fun i hi => hc.trans_lt (hb.trans_le (ha hi))

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns

Tactic:
Antitone.directed_le fun _ _ ↦ Set.Ici_subset_Ici.2

Premises used: Iff.mpr, Set.Ici_subset_Ici, Antitone.directed_le
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns

Tactic:
exact Antitone.directed_le fun _ _ ↦ Set.Ici_subset_Ici.2

Premises used: Iff.mpr, Set.Ici_subset_Ici, Antitone.directed_le
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ (a : ι), n ∈ ns a

Tactic:
fun n => ⟨n, le_rfl⟩

Premises used: le_rfl, Exists.intro
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ (a : ι), n ∈ ns a

Tactic:
exact fun n => ⟨n, le_rfl⟩
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
⊢ Indep (limsup s atBot) (limsup s atBot) μ

Tactic:
Kernel.indep_limsup_atBot_self h_le h_indep

Premises used: ProbabilityTheory.Kernel.indep_limsup_atBot_self, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
inst_3 : StandardBorelSpace Ω
hm : m ≤ m0
inst_4 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
⊢ CondIndep m (limsup s atBot) (limsup s atBot) hm μ

Tactic:
Kernel.indep_limsup_atBot_self h_le h_indep

Premises used: ProbabilityTheory.Kernel.indep_limsup_atBot_self, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
apply : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (a : α) ∂μα,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atBot_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)

Premises used: ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self', ProbabilityTheory.Kernel.indep_limsup_atBot_self, ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
      a
h₁ h₂ :
  ∀ (a : α) (ha : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)),
    IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)

Tactic:
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Premises used: ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
    using Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot h_le h_indep ht_tail

Premises used: MeasureTheory.ae_dirac_eq, ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot, Filter.eventually_pure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeInf ι
inst_1 : NoMinOrder ι
inst_2 : Nonempty ι
inst_3 : StandardBorelSpace Ω
hm : m ≤ m0
inst_4 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1

Tactic:
condExp_eq_zero_or_one_of_condIndepSet_self hm (limsup_le_iSup.trans (iSup_le h_le) t ht_tail)
    ((condIndep_limsup_atBot_self hm h_le h_indep).condIndepSet_of_measurableSet ht_tail ht_tail)

Premises used: ProbabilityTheory.CondIndep.condIndepSet_of_measurableSet, Filter.limsup_le_iSup, iSup_le, LE.le.trans, ProbabilityTheory.condIndep_limsup_atBot_self, ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.dirac (f a)

Tactic:
Measure.measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
refine :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((Measure.dirac (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.dirac (f a)

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 (f b)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((Measure.dirac (f b) : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
simp_rw [Measure.dirac_apply' _ hs]

Premises used: MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 (f b)

Tactic:
measurable_one.indicator (hf hs)

Premises used: Set.Mem, Set.indicator, Measurable.indicator, measurable_one
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 (f b)

Tactic:
exact measurable_one.indicator (hf hs)

Premises used: Measurable.indicator, measurable_one
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((deterministic f hf : (a : α) → Measure β) a : Measure β)
    (Measure.dirac (f a) : Measure β)

Tactic:
rfl

Premises used: MeasureTheory.Measure.dirac, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable, rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 (f a) : ℝ≥0∞)

Tactic:
simp_rw [Measure.dirac_apply' _ hs]

Premises used: MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → β
hf : Measurable f
h : f = g
⊢ deterministic f hf = deterministic g ⋯

Tactic:
grind
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (m0 := mβ) (Measure.dirac (f a))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
rw : ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
rw₁ rw₂ : f (g a) = f (g a)
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg : (a : α) → Measure β) a = f (g a)

Tactic:
rw [deterministic_apply, lintegral_dirac' _ hf]

Premises used: MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.deterministic_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst : MeasurableSingletonClass β
rw : ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)
rw₁ rw₂ : f (g a) = f (g a)
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg : (a : α) → Measure β) a = f (g a)

Tactic:
rw [deterministic_apply, lintegral_dirac (g a) f]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.lintegral_dirac
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
s : Set β
hs : MeasurableSet s
inst : Decidable (g a ∈ s)
rw : ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
rw₁ rw₂ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg : (a : α) → Measure β) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setLIntegral_dirac' hf hs]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.setLIntegral_dirac'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst : MeasurableSingletonClass β
s : Set β
inst_1 : Decidable (g a ∈ s)
rw : ∫⁻ (x : β) in s, f x ∂Measure.dirac (g a) = if g a ∈ s then f (g a) else 0
rw₁ rw₂ : (if g a ∈ s then f (g a) else 0) = if g a ∈ s then f (g a) else 0
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg : (a : α) → Measure β) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setLIntegral_dirac f s]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.setLIntegral_dirac
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel.{u_1, u_1} (α := α) (mα := mα) (deterministic id ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
rw : Eq (α := Measure α) ((deterministic id ⋯ : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)
rw₁ : Eq (α := Measure α) (Measure.dirac (id a)) (Measure.dirac a)
rw₂ rw₃ : Eq (α := Measure α) (Measure.dirac a) (Measure.dirac a)
⊢ Eq (α := Measure α) ((Kernel.id : (a : α) → Measure α) a : Measure α) (Measure.dirac a : Measure α)

Tactic:
rw [Kernel.id, deterministic_apply, id_def]

Premises used: id_def, ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.id
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
rw : ∫⁻ (a : α), f a ∂Measure.dirac a = f a
rw₁ rw₂ : f a = f a
⊢ ∫⁻ (a : α), f a ∂(Kernel.id : (a : α) → Measure α) a = f a

Tactic:
rw [id_apply, lintegral_dirac' _ hf]

Premises used: MeasureTheory.lintegral_dirac', ProbabilityTheory.Kernel.id_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
rw : ∫⁻ (a : α), f a ∂Measure.dirac a = f a
rw₁ rw₂ : f a = f a
⊢ ∫⁻ (a : α), f a ∂(Kernel.id : (a : α) → Measure α) a = f a

Tactic:
rw [id_apply, lintegral_dirac]

Premises used: MeasureTheory.lintegral_dirac, ProbabilityTheory.Kernel.id_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (mα := mα) (deterministic (fun (x : α) ↦ (x, x)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
⊢ Eq (α := Measure (α × α)) ((copy α : (a : α) → Measure (α × α)) a : Measure (α × α))
    (Measure.dirac (a, a) : Measure (α × α))

Tactic:
simp [copy, deterministic_apply]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.copy
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel.{u_1, u_4} (α := α) (β := PUnit.{u_4 + 1}) (mα := mα) (mβ := PUnit.instMeasurableSpace)
    (deterministic (fun (x : α) ↦ PUnit.unit) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
⊢ Eq.{u_4 + 1} (α := Measure PUnit.{u_4 + 1})
    ((discard α : (a : α) → Measure PUnit.{u_4 + 1}) a : Measure PUnit.{u_4 + 1})
    (Measure.dirac PUnit.unit : Measure PUnit.{u_4 + 1})

Tactic:
deterministic_apply _ _

Premises used: ProbabilityTheory.Kernel.deterministic_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (α := α × β) (mα := Prod.instMeasurableSpace) (deterministic Prod.swap ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
rw :
  Eq (α := Measure (β × α)) ((deterministic Prod.swap ⋯ : (a : α × β) → Measure (β × α)) ab : Measure (β × α))
    (Measure.dirac ab.swap : Measure (β × α))
rw₁ rw₂ : Eq (α := Measure (β × α)) (Measure.dirac ab.swap) (Measure.dirac ab.swap)
⊢ Eq (α := Measure (β × α)) ((swap α β : (a : α × β) → Measure (β × α)) ab : Measure (β × α))
    (Measure.dirac ab.swap : Measure (β × α))

Tactic:
rw [swap, deterministic_apply]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.swap
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
s : Set (β × α)
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((Measure.dirac ab.swap : (a : Set (β × α)) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 ab.swap : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) (s.indicator 1 ab.swap) (s.indicator 1 ab.swap)
⊢ Eq (α := ℝ≥0∞)
    ((((swap α β : (a : α × β) → Measure (β × α)) ab : Measure (β × α)) : (a : Set (β × α)) → ℝ≥0∞) s : ℝ≥0∞)
    (s.indicator 1 ab.swap : ℝ≥0∞)

Tactic:
rw [swap_apply, Measure.dirac_apply' _ hs]

Premises used: ProbabilityTheory.Kernel.swap_apply, MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μβ : Measure β
a : α
⊢ ((const α μβ : Kernel α β) : (a : α) → Measure β) a = μβ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
h :
  ∀ (x : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((const α 0 : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α β) : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α β) (const α 0) 0

Tactic:
ext x s _
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((const α 0 : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst : MeasurableSpace β
μ ν : Measure α
h :
  ∀ (a : β) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((((const β (μ + ν) : Kernel β α) : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((((HAdd.hAdd (α := Kernel β α) (const β μ) (const β ν) : (a : β) → Measure α) a : Measure α) :
              (a : Set α) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ const β (μ + ν) = HAdd.hAdd (α := Kernel β α) (const β μ) (const β ν)

Tactic:
ext