awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
rw :
  HMul.hMul (β := ENNReal)
      (HMul.hMul (β := ENNReal)
        (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
    HMul.hMul (β := ENNReal)
      (HMul.hMul (β := ENNReal)
        (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
| HMul.hMul (α := ENNReal) (β := ENNReal) ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal)
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) *
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ s) : ENNReal) +
    HMul.hMul (α := ENNReal) (β := ENNReal) ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal)
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal) *
      HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
        (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ t) : ENNReal)

Tactic:
rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_assoc]

Premises used: mul_assoc, Inv.inv, mul_comm, Set.union_inter_cancel_left, Union.union, MeasureTheory.Measure.count, DFunLike.coe, Set.union_inter_cancel_right
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr :
  HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
      (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ u) : ENNReal)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) *
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ s) : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal) *
        HMul.hMul (α := ENNReal) (β := ENNReal)
          ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ t) : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
      (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ u) : ENNReal)

Tactic:
conv_lhs =>
    rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_assoc]

Premises used: mul_assoc, Inv.inv, mul_comm, Set.union_inter_cancel_left, Union.union, MeasureTheory.Measure.count, DFunLike.coe, Set.union_inter_cancel_right
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
inr : Disjoint (s ∩ u) (t ∩ u)
inr₁ : MeasurableSet (t ∩ u)
inr₂ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
inr₃ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (⊤ : ENNReal)
inr₄ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
inr₅ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) +
      HMul.hMul (β := ENNReal)
        (HMul.hMul (β := ENNReal)
          (HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
            ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t)⁻¹ : ENNReal))
          (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) : ENNReal))
        ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal)
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∪ t))⁻¹ : ENNReal)
      (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ((s ∪ t) ∩ u) : ENNReal)

Tactic:
rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_comm]

Premises used: add_mul, ENNReal.mul_inv_cancel, mul_comm, MeasureTheory.measure_union, Set.union_inter_distrib_right, one_mul
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Disjoint (s ∩ u) (t ∩ u)

Tactic:
hst.mono inf_le_left inf_le_left

Premises used: Disjoint.mono, inf_le_left
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ MeasurableSet (t ∩ u)

Tactic:
(ht.inter_of_left _).measurableSet

Premises used: Set.Finite.inter_of_left, Set.Finite.measurableSet
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)

Tactic:
Measure.count_ne_zero ht'

Premises used: MeasureTheory.Measure.count_ne_zero
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (⊤ : ENNReal)

Tactic:
(Measure.count_apply_lt_top.2 ht).ne

Premises used: Iff.mpr, MeasureTheory.Measure.count_apply_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
Measure.count_ne_zero hs'

Premises used: MeasureTheory.Measure.count_ne_zero
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
(Measure.count_apply_lt_top.2 hs).ne

Premises used: Iff.mpr, MeasureTheory.Measure.count_apply_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ Disjoint (s ∩ u) (t ∩ u)

Tactic:
exacts [hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet,
    Measure.count_ne_zero ht', (Measure.count_apply_lt_top.2 ht).ne, Measure.count_ne_zero hs',
    (Measure.count_apply_lt_top.2 hs).ne]

Premises used: MeasureTheory.Measure.count_ne_zero, Iff.mpr, Set.Finite.inter_of_left, MeasureTheory.Measure.count_apply_lt_top, Disjoint.mono, inf_le_left, Set.Finite.measurableSet, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ s = s ∩ u ∪ s ∩ uᶜ

Tactic:
simp
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
rw :
  HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) +
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
      (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ uᶜ) : ENNReal)
| ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t

Tactic:
rw [(by simp : s = s ∩ u ∪ s ∩ uᶜ),
      ← uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right)]

Premises used: Set.Finite.inter_of_left, inf_le_right, disjoint_compl_right, Disjoint.mono, ProbabilityTheory.uniformOn_disjoint_union
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
conv_rhs :
  HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) uᶜ : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ uᶜ) : ENNReal)
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) uᶜ : ENNReal) =
    ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t

Tactic:
conv_rhs =>
    rw [(by simp : s = s ∩ u ∪ s ∩ uᶜ),
      ← uniformOn_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right)]

Premises used: Set.Finite.inter_of_left, inf_le_right, disjoint_compl_right, Disjoint.mono, ProbabilityTheory.uniformOn_disjoint_union
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) uᶜ : ENNReal) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ u) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ u) : ENNReal) +
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
        (((uniformOn (s ∩ u ∪ s ∩ uᶜ) : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ uᶜ) : ENNReal)

Tactic:
simp [uniformOn_inter_self hs]

Premises used: ProbabilityTheory.uniformOn_inter_self
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f : ι → Set Ω
⊢ Eq (α := Measure ((i : ι) → Ω)) (uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f))
    (Measure.pi (α := fun (i : ι) ↦ Ω) fun (i : ι) ↦ uniformOn (f i))

Tactic:
(MeasureTheory.Measure.pi_eq fun t ht ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f : ι → Set Ω
refine :
  ∀ (t : (i : ι) → Set Ω) (ht : ∀ (i : ι), MeasurableSet (t i)),
    Eq (α := ENNReal)
      ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f) : (a : Set ((i : ι) → Ω)) → ENNReal)
          (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
        ENNReal)
      (∏ i : ι, ((uniformOn (f i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)
⊢ Eq (α := Measure ((i : ι) → Ω)) (uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f))
    (Measure.pi (α := fun (i : ι) ↦ Ω) fun (i : ι) ↦ uniformOn (f i))

Tactic:
refine (MeasureTheory.Measure.pi_eq fun t ht ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f t : (i : ι) → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (i : ι), (f i).Finite

Tactic:
simp [Set.toFinite]

Premises used: Set.toFinite
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f t : (i : ι) → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
lift :
  ∀ (f : (i : ι) → Finset Ω),
    Eq (α := ENNReal)
      ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
            (a : Set ((i : ι) → Ω)) → ENNReal)
          (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
        ENNReal)
      (∏ i : ι, ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ f) : (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
      ENNReal)
    (∏ i : ι, ((uniformOn (f i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)

Tactic:
lift f to ι → Finset Ω using by simp [Set.toFinite]
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
t : (i : ι) → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → Finset Ω
⊢ ∀ (i : ι), (t i).Finite

Tactic:
simp [Set.toFinite]

Premises used: Set.toFinite
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
t : (i : ι) → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → Finset Ω
lift :
  ∀ (t : (i : ι) → Finset Ω) (ht : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i)),
    Eq (α := ENNReal)
      ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
            (a : Set ((i : ι) → Ω)) → ENNReal)
          (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(t i) : Set Ω)) :
        ENNReal)
      (∏ i : ι,
          ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal)
            ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i) :
        ENNReal)
⊢ Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
          (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ t) :
      ENNReal)
    (∏ i : ι, ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal) (t i) : ENNReal)

Tactic:
lift t to ι → Finset Ω using by simp [Set.toFinite]
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f t : (i : ι) → Finset Ω
ht : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i)
⊢ Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
          (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(t i) : Set Ω)) :
      ENNReal)
    (∏ i : ι,
        ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i) :
      ENNReal)

Tactic:
simp [← Fintype.coe_piFinset, uniformOn_apply_finset, ← Fintype.piFinset_inter,
    ENNReal.prod_div_distrib_of_ne_top]

Premises used: ProbabilityTheory.uniformOn_apply_finset, ENNReal.prod_div_distrib_of_ne_top, Fintype.coe_piFinset, Fintype.piFinset_inter
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ι : Type u_2
inst_2 : Fintype ι
inst_3 : Finite Ω
f t : (i : ι) → Finset Ω
ht : ∀ (i : ι), MeasurableSet.{u_1} (α := Ω) ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i)
⊢ Eq (α := ENNReal)
    ((uniformOn (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(f i) : Set Ω)) :
          (a : Set ((i : ι) → Ω)) → ENNReal)
        (Set.pi (α := fun (i : ι) ↦ Ω) Set.univ fun (i : ι) ↦ (↑(t i) : Set Ω)) :
      ENNReal)
    (∏ i : ι,
        ((uniformOn ((fun (i : ι) ↦ (↑(f i) : Set Ω)) i) : Measure Ω) : (a : Set Ω) → ENNReal)
          ((fun (i : ι) ↦ (↑(t i) : Set Ω)) i) :
      ENNReal)

Tactic:
classical
  simp [← Fintype.coe_piFinset, uniformOn_apply_finset, ← Fintype.piFinset_inter,
    ENNReal.prod_div_distrib_of_ne_top]

Premises used: ProbabilityTheory.uniformOn_apply_finset, ENNReal.prod_div_distrib_of_ne_top, Fintype.coe_piFinset, Fintype.piFinset_inter
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
h :
  ∀ (a a_1 : X.V),
    Eq.{u + 1} (α := k)
      (((Finsupp.lmapDomain k k
                    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) 1)) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) ∘ₗ
                  Finsupp.lsingle a :
                (a : k) → X.V →₀ k)
              1 :
            (a : X.V) → k)
          a_1 :
        k)
      (((1 ∘ₗ Finsupp.lsingle a : (a : k) → X.V →₀ k) 1 : (a : X.V) → k) a_1 : k)
⊢ Eq (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
    (Finsupp.lmapDomain k k
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) 1)) :
        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
a a_1 : X.V
⊢ Eq.{u + 1} (α := k)
    (((Finsupp.lmapDomain k k
                  (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) 1)) :
                    (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a_1 :
      k)
    (((1 ∘ₗ Finsupp.lsingle a : (a : k) → X.V →₀ k) 1 : (a : X.V) → k) a_1 : k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x x_1 : G
h :
  ∀ (a a_1 : X.V),
    Eq.{u + 1} (α := k)
      (((Finsupp.lmapDomain k k
                    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) (x * x_1))) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) ∘ₗ
                  Finsupp.lsingle a :
                (a : k) → X.V →₀ k)
              1 :
            (a : X.V) → k)
          a_1 :
        k)
      (((HMul.hMul (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
                    (Finsupp.lmapDomain k k
                      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x)) :
                        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
                    (Finsupp.lmapDomain k k
                      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1)) :
                        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V)) ∘ₗ
                  Finsupp.lsingle a :
                (a : k) → X.V →₀ k)
              1 :
            (a : X.V) → k)
          a_1 :
        k)
⊢ Finsupp.lmapDomain k k
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) (x * x_1))) :
        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) =
    HMul.hMul (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
      (Finsupp.lmapDomain k k
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x)) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
      (Finsupp.lmapDomain k k
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1)) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))

Tactic:
ext