awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
intro : ∀ (val : Encodable β), extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)
⊢ extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
intro :
  extend (P := P) m (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b) =
    ∑' (i : ℕ), extend (P := P) m (⋃ b ∈ Encodable.decode₂ β i, f b)
intro₁ : extend (P := P) m ∅ = 0
⊢ extend (P := P) m (⋃ (i : β), f i) = ∑' (i : β), extend (P := P) m (f i)

Tactic:
rw [← Encodable.iUnion_decode₂, ← tsum_iUnion_decode₂]

Premises used: Encodable.iUnion_decode₂, tsum_iUnion_decode₂
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
⊢ extend (P := P) m (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b) =
    ∑' (i : ℕ), extend (P := P) m (⋃ b ∈ Encodable.decode₂ β i, f b)

Tactic:
extend_iUnion_nat PU (fun n => Encodable.iUnion_decode₂_cases P0 hm)
        (mU _ (Encodable.iUnion_decode₂_disjoint_on hd))

Premises used: Encodable.iUnion_decode₂_cases, Encodable.iUnion_decode₂_disjoint_on, MeasureTheory.extend_iUnion_nat
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
⊢ extend (P := P) m (⋃ (i : ℕ), ⋃ b ∈ Encodable.decode₂ β i, f b) =
    ∑' (i : ℕ), extend (P := P) m (⋃ b ∈ Encodable.decode₂ β i, f b)

Tactic:
exact
      extend_iUnion_nat PU (fun n => Encodable.iUnion_decode₂_cases P0 hm)
        (mU _ (Encodable.iUnion_decode₂_disjoint_on hd))

Premises used: Encodable.iUnion_decode₂_cases, Encodable.iUnion_decode₂_disjoint_on, MeasureTheory.extend_iUnion_nat
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
⊢ extend (P := P) m ∅ = 0

Tactic:
extend_empty P0 m0

Premises used: MeasureTheory.extend_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val : Encodable β
⊢ extend (P := P) m ∅ = 0

Tactic:
exact extend_empty P0 m0

Premises used: MeasureTheory.extend_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
rw : ∑ b : Bool, extend (P := P) m (bif b then s₁ else s₂) = extend (P := P) m s₁ + extend (P := P) m s₂
⊢ extend (P := P) m (s₁ ∪ s₂) = extend (P := P) m s₁ + extend (P := P) m s₂

Tactic:
rw [union_eq_iUnion,
    extend_iUnion P0 m0 PU mU (pairwise_disjoint_on_bool.2 hd) (Bool.forall_bool.2 ⟨h₂, h₁⟩),
    tsum_fintype]

Premises used: Iff.mpr, Bool.forall_bool, And.intro, tsum_fintype, pairwise_disjoint_on_bool, MeasureTheory.extend_iUnion, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ ∑ b : Bool, extend (P := P) m (bif b then s₁ else s₂) = extend (P := P) m s₁ + extend (P := P) m s₂

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
μ : OuterMeasure α
⊢ μ ≤ inducedOuterMeasure (P := P) m P0 m0 ↔ ∀ (s : Set α) (hs : P s), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s hs

Tactic:
le_ofFunction.trans <| forall_congr' fun _s => le_iInf_iff

Premises used: le_iInf_iff, forall_congr', Iff.trans, MeasureTheory.OuterMeasure.le_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
ofFunction_union_of_top_of_nonempty_inter fun u hsu htu => @iInf_of_empty _ _ _ ⟨h u hsu htu⟩ _

Premises used: iInf_of_empty, MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : P s
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s = extend (P := P) m s

Tactic:
ofFunction_eq s (fun _t => extend_mono' m_mono hs) (extend_iUnion_le_tsum_nat' PU msU)

Premises used: MeasureTheory.extend_mono', MeasureTheory.OuterMeasure.ofFunction_eq, MeasureTheory.extend_iUnion_le_tsum_nat'
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : P s
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s = m s hs

Tactic:
(inducedOuterMeasure_eq_extend' PU msU m_mono hs).trans <| extend_eq _ _

Premises used: MeasureTheory.extend_eq, Eq.trans, MeasureTheory.inducedOuterMeasure_eq_extend'
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
a :
  LE.le (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
a₁ :
  LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
a : ∀ (i : Set α) (i_1 : P i) (i_2 : s ⊆ i), (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s ≤ m i i_1
⊢ LE.le (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)

Tactic:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
a : (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤ m t ht
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s ≤ m t ht

Tactic:
grw [hs]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤ m t ht

Tactic:
le_of_eq (inducedOuterMeasure_eq' _ msU m_mono _)

Premises used: MeasureTheory.inducedOuterMeasure_eq', le_of_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s t : Set α
ht : P t
hs : s ⊆ t
⊢ (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t ≤ m t ht

Tactic:
exact le_of_eq (inducedOuterMeasure_eq' _ msU m_mono _)

Premises used: MeasureTheory.inducedOuterMeasure_eq', le_of_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_iInf ?_

Premises used: iInf, le_iInf, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
a :
  ∀ (i : ℕ → Set α),
    LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht)
      (⨅ (_ : s ⊆ ⋃ (i_1 : ℕ), i i_1), ∑' (i_1 : ℕ), extend (P := P) m (i i_1))
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht)
    (⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), extend (P := P) m (f i))

Tactic:
le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
a :
  ∀ (i : s ⊆ ⋃ (i : ℕ), f i),
    LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht) (∑' (i : ℕ), extend (P := P) m (f i))
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht)
    (⨅ (_ : s ⊆ ⋃ (i : ℕ), f i), ∑' (i : ℕ), extend (P := P) m (f i))

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht) (∑' (i : ℕ), extend (P := P) m (f i))

Tactic:
le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)

Premises used: MeasureTheory.extend_iUnion_le_tsum_nat', le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
a : ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ extend (P := P) m (⋃ (i : ℕ), f i)
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht) (∑' (i : ℕ), extend (P := P) m (f i))

Tactic:
refine le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)

Premises used: MeasureTheory.extend_iUnion_le_tsum_nat', le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
⊢ ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ extend (P := P) m (⋃ (i : ℕ), f i)

Tactic:
le_iInf ?_

Premises used: MeasureTheory.extend, le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
a : ∀ (i : P (⋃ (i : ℕ), f i)), ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ m (⋃ (i : ℕ), f i) i
⊢ ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ extend (P := P) m (⋃ (i : ℕ), f i)

Tactic:
refine le_iInf ?_

Premises used: le_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
h2f : P (⋃ (i : ℕ), f i)
⊢ ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ m (⋃ (i : ℕ), f i) h2f

Tactic:
iInf_le_of_le _ (iInf_le_of_le h2f <| iInf_le _ hf)

Premises used: iInf_le_of_le, iInf_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ (i : ℕ), f i
h2f : P (⋃ (i : ℕ), f i)
⊢ ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ m (⋃ (i : ℕ), f i) h2f

Tactic:
exact iInf_le_of_le _ (iInf_le_of_le h2f <| iInf_le _ hf)

Premises used: iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
Pu : P univ
⊢ Eq (α := ℝ≥0∞) ((fun (x : Set α) (x_1 : P x) ↦ (0 : ℝ≥0∞)) ∅ P0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
h :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) (fun (x : Set α) (x_1 : P x) ↦ 0) P0 ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ inducedOuterMeasure (P := P) (fun (x : Set α) (x_1 : P x) ↦ 0) P0 ⋯ = 0

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
s : Set α
x : ℕ → Set α
h : ∀ (i : ℕ), P (x i)
⊢ LE.le (α := ℝ≥0∞) 0 (∑' (i : ℕ), 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
s x x_1 : Set α
⊢ ∀ (hs₁ : P x) (hs₂ : P x_1), x ⊆ x_1 → LE.le (α := ℝ≥0∞) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
s : Set α
h :
  Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : P t), ⨅ (_ : s ⊆ t), 0 : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) (fun (x : Set α) (x_1 : P x) ↦ 0) P0 ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [inducedOuterMeasure_eq_iInf PU (fun _ _ => by simp) (fun _ _ => by simp)]

Premises used: MeasureTheory.inducedOuterMeasure_eq_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
s : Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : s ⊆ univ), 0 : ℝ≥0∞) (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
Pu : P univ
s : Set α
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : P t), ⨅ (_ : s ⊆ t), 0 : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact le_antisymm (iInf₂_le_of_le univ Pu (by simp)) zero_le

Premises used: zero_le, Set.univ, iInf₂_le_of_le, le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A : Set α
rw :
  Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → α) ⁻¹' A) : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [inducedOuterMeasure_eq_iInf _ msU m_mono, inducedOuterMeasure_eq_iInf _ msU m_mono]

Premises used: MeasureTheory.inducedOuterMeasure_eq_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A : Set α
symm :
  Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)

Tactic:
symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
f : α ≃ α
Pm : ∀ (s : Set α), P ((⇑f : (a : α) → α) ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m ((⇑f : (a : α) → α) ⁻¹' s) ⋯ = m s hs
A : Set α
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht)
    (⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : (⇑f : (a : α) → α) ⁻¹' A ⊆ t), m t ht)

Tactic:
f.injective.preimage_surjective.iInf_congr (preimage f) fun s => ?_

Premises used: Function.Injective.preimage_surjective, Set.preimage, Function.Surjective.iInf_congr, Equiv.injective, DFunLike.coe