awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
rw : μ₁.trim + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
rw₁ : μ₁.toOuterMeasure + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
rw₂ rw₃ : μ₁.toOuterMeasure + μ₂.toOuterMeasure ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
⊢ (μ₁.toOuterMeasure + μ₂.toOuterMeasure).trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure

Tactic:
rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed]

Premises used: MeasureTheory.Measure.trimmed, MeasureTheory.OuterMeasure.trim_add
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ (μ₁ + μ₂).toOuterMeasure = μ₁.toOuterMeasure + μ₂.toOuterMeasure

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ (⇑(μ₁ + μ₂) : (a : Set α) → ℝ≥0∞) =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (⇑μ₁ : (a : Set α) → ℝ≥0∞) (⇑μ₂ : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
μ₁ μ₂ : Measure α
s : Set α
⊢ (μ₁ + μ₂ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: WithTop.map₂, rfl, Option.map₂
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x : MeasurableSpace α
c : R
μ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ Eq (α := ℝ≥0∞) ((c • μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
    (∑' (i : ℕ), (c • μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp only [OuterMeasure.smul_apply, coe_toOuterMeasure, ENNReal.tsum_const_smul,
          measure_iUnion hd hs]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, MeasureTheory.measure_iUnion, ENNReal.tsum_const_smul, MeasureTheory.OuterMeasure.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x : MeasurableSpace α
c : R
μ : Measure α
rw : c • μ.trim ≤ c • μ.toOuterMeasure
rw₁ rw₂ : c • μ.toOuterMeasure ≤ c • μ.toOuterMeasure
⊢ (c • μ.toOuterMeasure).trim ≤ c • μ.toOuterMeasure

Tactic:
rw [OuterMeasure.trim_smul, μ.trimmed]

Premises used: MeasureTheory.OuterMeasure.trim_smul, MeasureTheory.Measure.trimmed
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
R : Type u_6
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
_m : MeasurableSpace α
c : R
μ : Measure α
⊢ (c • μ).toOuterMeasure = c • μ.toOuterMeasure

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
R : Type u_6
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
_m : MeasurableSpace α
c : R
μ : Measure α
⊢ (⇑(c • μ) : (a : Set α) → ℝ≥0∞) = HSMul.hSMul (β := (a : Set α) → ℝ≥0∞) c (⇑μ : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0
μ : Measure α
⊢ (↑c : ℝ≥0∞) • μ = c • μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
R : Type u_6
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
_m : MeasurableSpace α
c : R
μ : Measure α
s : Set α
⊢ (c • μ : (a : Set α) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
inst_5 : SMulCommClass R R' ℝ≥0∞
x : MeasurableSpace α
⊢ SMulCommClass.{u_6, u_7, u_1} R R' (Measure α)

Tactic:
⟨fun _ _ _ => ext fun _ _ => smul_comm _ _ _⟩

Premises used: MeasureTheory.Measure.toOuterMeasure, SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe, MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
inst_5 : SMul R R'
inst_6 : IsScalarTower R R' ℝ≥0∞
x : MeasurableSpace α
⊢ IsScalarTower.{u_6, u_7, u_1} R R' (Measure α)

Tactic:
⟨fun _ _ _ => ext fun _ _ => smul_assoc _ _ _⟩

Premises used: smul_assoc, MeasureTheory.Measure.toOuterMeasure, IsScalarTower.mk, DFunLike.coe, MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
inst_5 : SMul Rᵐᵒᵖ ℝ≥0∞
inst_6 : IsCentralScalar R ℝ≥0∞
x : MeasurableSpace α
⊢ IsCentralScalar.{u_6, u_1} R (Measure α)

Tactic:
⟨fun _ _ => ext fun _ _ => op_smul_eq_smul _ _⟩

Premises used: MeasureTheory.Measure.toOuterMeasure, IsCentralScalar.mk, DFunLike.coe, MeasureTheory.Measure.ext, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
⊢ Eq (α := Set α → ℝ≥0∞) ((coeAddHom : (a : Measure α) → Set α → ℝ≥0∞) μ : Set α → ℝ≥0∞)
    ((⇑μ : (a : Set α) → ℝ≥0∞) : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
_m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
⊢ Eq.{u_1 + 1} (α := (a : Set α) → ℝ≥0∞) (⇑(∑ i ∈ I, μ i) : (a : Set α) → ℝ≥0∞) (∑ i ∈ I, (⇑(μ i) : (a : Set α) → ℝ≥0∞))

Tactic:
map_sum coeAddHom μ I

Premises used: MeasureTheory.Measure.coeAddHom, map_sum
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((∑ i ∈ I, (⇑(μ i) : (a : Set α) → ℝ≥0∞)) s) (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s)
rw₁ rw₂ : Eq (α := ℝ≥0∞) (∑ c ∈ I, (μ c : (a : Set α) → ℝ≥0∞) s) (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (((∑ i ∈ I, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [coe_finsetSum, Finset.sum_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : Semiring R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
⊢ ∀ (r : R) (m : Measure α),
    (⇑(r • m) : (a : Set α) → ℝ≥0∞) = HSMul.hSMul (β := (a : Set α) → ℝ≥0∞) r (⇑m : (a : Set α) → ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
μ : Measure α
⊢ c • μ = 0 ↔ c = 0 ∨ μ = 0

Tactic:
simp [Measure.ext_iff', forall_or_left]

Premises used: forall_or_left, MeasureTheory.Measure.ext_iff'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
c : ℝ≥0
μ : Measure α
s : Set α
⊢ (c • μ : (a : Set α) → ℝ≥0∞) s = HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
c : ℝ≥0
μ : Measure α
s : Set α
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
rw : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) = 0
rw₁ : HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
rw₂ : HSMul.hSMul (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) c 1) 0 = 0
rw₃ rw₄ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]

Premises used: smul_zero, MeasureTheory.ae_iff, smul_one_smul, ENNReal, MeasureTheory.Measure.smul_apply, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ ae (c • μ) ≤ ae μ

Tactic:
fun _ h ↦ ae_smul_measure h c

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Measure.ae_smul_measure
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
p : α → Prop
hc : c ≠ 0
μ : Measure α
⊢ (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

Tactic:
simp [ae_iff, hc]

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
h : ∀ (s : Set α), s ∈ ae (c • μ) ↔ s ∈ ae μ
⊢ ae (c • μ) = ae μ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
s : Set α
⊢ s ∈ ae (c • μ) ↔ s ∈ ae μ

Tactic:
ae_smul_measure_iff hc

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Measure.ae_smul_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
s : Set α
⊢ s ∈ ae (c • μ) ↔ s ∈ ae μ

Tactic:
exact ae_smul_measure_iff hc

Premises used: MeasureTheory.Measure.ae_smul_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
p : α → Prop
hc : c ≠ 0
μ : Measure α
⊢ (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

Tactic:
simp [ae_iff, hc]

Premises used: MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
hc : c ≠ 0
μ : Measure α
h : ∀ (s : Set α), s ∈ ae (c • μ) ↔ s ∈ ae μ
⊢ ae (c • μ) = ae μ

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
hc : c ≠ 0
μ : Measure α
s : Set α
⊢ s ∈ ae (c • μ) ↔ s ∈ ae μ

Tactic:
ae_ennreal_smul_measure_iff hc

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Measure.ae_ennreal_smul_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
hc : c ≠ 0
μ : Measure α
s : Set α
⊢ s ∈ ae (c • μ) ↔ s ∈ ae μ

Tactic:
exact ae_ennreal_smul_measure_iff hc

Premises used: MeasureTheory.Measure.ae_ennreal_smul_measure_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
le_antisymm (measure_mono h') ?_

Premises used: le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
refine le_antisymm (measure_mono h') ?_

Premises used: le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
have : μ t + ν t ≤ μ s + ν t :=
    calc
      μ t + ν t = μ s + ν s := h''.symm
      _ ≤ μ s + ν t := by gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
this :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
apply : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply ENNReal.le_of_add_le_add_right _ this

Premises used: ENNReal.le_of_add_le_add_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
this :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_top_of_le_ne_top h (le_add_left le_rfl)

Premises used: le_rfl, ne_top_of_le_ne_top, le_add_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
this :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_top_of_le_ne_top h (le_add_left le_rfl)

Premises used: le_rfl, ne_top_of_le_ne_top, le_add_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [add_comm] at h'' h

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s ⊆ t

Tactic:
rw [add_comm] at h'' h

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h'₁ : s ⊆ t
⊢ Eq (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [add_comm] at h'' h

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_eq_left_of_subset_of_measure_add_eq h h' h''

Premises used: MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact measure_eq_left_of_subset_of_measure_add_eq h h' h''

Premises used: MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
(measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm

Premises used: MeasureTheory.subset_toMeasurable, Eq.symm, MeasureTheory.Measure.measure_inter_eq_of_measure_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞)
refine_2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm

Premises used: MeasureTheory.subset_toMeasurable, Eq.symm, MeasureTheory.Measure.measure_inter_eq_of_measure_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞)

Tactic:
measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm

Premises used: MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞)

Tactic:
refine
      measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm

Premises used: MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht refine_1 refine_1₁ refine_1₂ refine_1₃ : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [measure_toMeasurable t]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht

Premises used: ENNReal.add_eq_top, Ne, MeasureTheory.Measure.coe_add, not_or, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht :
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ht.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht :
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ht.1

Premises used: And.left