awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 ∨ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 ∨ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hνs.imp_right fun hs ↦ h hs

Premises used: Or.imp_right
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 ∨ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 ∨ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hνs.imp_right fun hs ↦ h hs

Premises used: Or.imp_right
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs : Eq (α := ℝ≥0∞) ((ν + ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
simp :
  ∀
    (hs :
      Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ₁ + μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, add_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs :
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨h1 hs.1, h2 hs.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
s : Set α
hs :
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨h1 hs.1, h2 hs.2⟩
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, And.right, And.left, Iff.intro, MeasureTheory.Measure.AbsolutelyContinuous.add
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
refine_1 : ∀ (h : μ₁ + μ₂ ≪ ν), μ₁ ≪ ν ∧ μ₂ ≪ ν
refine_2 : ∀ (h : μ₁ ≪ ν ∧ μ₂ ≪ ν), ν + ν ≪ ν
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
s : Set α
hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa using h hs0
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
this :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
this :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
refine_2 : HSMul.hSMul (α := ℝ≥0) 2 ν ≪ ν
⊢ ν + ν ≪ ν

Tactic:
rw [← two_smul ℝ≥0]

Premises used: two_smul, NNReal
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ HSMul.hSMul (α := ℝ≥0) 2 ν ≪ ν

Tactic:
AbsolutelyContinuous.rfl.smul_left 2

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, MeasureTheory.Measure.AbsolutelyContinuous.rfl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ HSMul.hSMul (α := ℝ≥0) 2 ν ≪ ν

Tactic:
exact AbsolutelyContinuous.rfl.smul_left 2

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, MeasureTheory.Measure.AbsolutelyContinuous.rfl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h₁ : μ₁ ≪ ν
h₂ : μ₂ ≪ ν
⊢ μ₁ + μ₂ ≪ ν

Tactic:
Measure.AbsolutelyContinuous.add_left_iff.mpr ⟨h₁, h₂⟩

Premises used: Iff.mpr, MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff, And.intro
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((ν + ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, add_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs :
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h1 hs.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
ν' : Measure α
s : Set α
hs :
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact h1 hs.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν' : Measure α
h : μ ≪ ν'
ν : Measure α
⊢ μ ≪ ν + ν'

Tactic:
simp [add_comm, add_right h]

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.add_right, add_comm
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
t : Set α
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hμν ht
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
t : Set α
ht : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
contrapose! :
  ∀ (ht : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
contrapose! ht
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
t : Set α
ht : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_all [hμν.null_mono]

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.null_mono
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ μ ≪ 0 ↔ μ = 0

Tactic:
⟨fun h ↦ measure_univ_eq_zero.mp (h rfl), fun h ↦ h.symm ▸ AbsolutelyContinuous.zero _⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.zero, Eq.rec, Iff.intro, Iff.mp, MeasureTheory.Measure.measure_univ_eq_zero, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
hμs : ∀ (i : ι), μs i ≪ ν
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((sum μs : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [sum_apply _ hs, fun i ↦ hμs i hs0]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
⊢ ν ≪ sum μs

Tactic:
AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (hs0 : Eq (α := ℝ≥0∞) ((sum μs : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ν ≪ sum μs

Tactic:
refine AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : Eq (α := ℝ≥0∞) ((sum μs : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (i : ι), Eq (α := ℝ≥0∞) ((μs i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [sum_apply _ hs, ENNReal.tsum_eq_zero] at hs0

Premises used: MeasureTheory.Measure.sum_apply, ENNReal.tsum_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μs i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hνμ (hs0 i)
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
ι : Type u_4
mα : MeasurableSpace α
ν : Measure α
μs : ι → Measure α
i : ι
hνμ : ν ≪ μs i
s : Set α
hs : MeasurableSet s
hs0 : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μs i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hνμ (hs0 i)
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ c • μ ≪ μ

Tactic:
.smul_left .rfl _

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ μ' : Measure α
c : ℝ≥0∞
hμ'_le : μ' ≤ c • μ
⊢ μ' ≪ μ

Tactic:
(Measure.absolutelyContinuous_of_le hμ'_le).trans smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.smul_absolutelyContinuous, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
hc : c ≠ 0
⊢ μ ≪ c • μ

Tactic:
simp [AbsolutelyContinuous, hc]

Premises used: MeasureTheory.Measure.AbsolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
⊢ μ ≪ c • ν

Tactic:
(absolutelyContinuous_smul hc).trans (hμν.smul c)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.absolutelyContinuous_smul, MeasureTheory.Measure.AbsolutelyContinuous.smul
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
rw : (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_eq_zero_iff_ae_notMem, measure_eq_zero_iff_ae_notMem]

Premises used: MeasureTheory.measure_eq_zero_iff_ae_notMem
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s

Tactic:
fun hs => h hs

Premises used: Filter.Eventually
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s

Tactic:
exact fun hs => h hs
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
δ : Type u_3
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
f g : α → δ
h' : f =ᶠ[ae ν] g
⊢ f =ᶠ[ae μ] g

Tactic:
h.ae_le h'

Premises used: Filter.Eventually, Filter.EventuallyEq, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
ν : Measure α
h' : ν ≪ μ
⊢ AEDisjoint ν s t

Tactic:
h' h

Premises used: MeasureTheory.AEDisjoint
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
ν : Measure α
h' : ν ≤ μ
⊢ AEDisjoint ν s t

Tactic:
h.of_absolutelyContinuous (Measure.absolutelyContinuous_of_le h')

Premises used: MeasureTheory.Measure.absolutelyContinuous_of_le, MeasureTheory.AEDisjoint.of_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≤ ν
⊢ ae μ ≤ ae ν

Tactic:
h.absolutelyContinuous.ae_le

Premises used: LE.le.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : Eq (α := ENNReal) (((map f ν : Measure β) : (a : Set β) → ENNReal) t : ENNReal) (0 : ENNReal)
rw :
  ∀ (ht : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) (((map f μ : Measure β) : (a : Set β) → ENNReal) t : ENNReal) (0 : ENNReal)

Tactic:
rw [hf.map_apply] at ht ⊢

Premises used: MeasurableEmbedding.map_apply
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)

Tactic:
hμν ht
-- Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (f ⁻¹' t) : ENNReal) (0 : ENNReal)

Tactic:
exact hμν ht
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
⊢ Eq.{u_2 + 1} (α := G) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
⊢ ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), Eq.{u_2 + 1} (α := G) 0 (∑ u ∈ I, 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m m' : AddContent G C
h :
  Eq (α := (a : Set α) → G) ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m)
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m')
mk :
  ∀ (toFun : Set α → G) (empty' : toFun ∅ = 0)
    (sUnion' :
      ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
        (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun u),
    Eq (α := (a : Set α) → G)
        ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
        ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m') →
      AddContent.mk (C := C) toFun empty' sUnion' = m'
⊢ m = m'

Tactic:
cases m
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m' : AddContent G C
toFun : Set α → G
empty' : toFun ∅ = 0
sUnion' :
  ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun u
h :
  Eq (α := (a : Set α) → G)
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) m')
mk :
  ∀ (toFun_1 : Set α → G) (empty'_1 : toFun_1 ∅ = 0)
    (sUnion'_1 :
      ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
        (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun_1 (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun_1 u),
    Eq (α := (a : Set α) → G)
        ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
        ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s)
          (AddContent.mk (C := C) toFun_1 empty'_1 sUnion'_1)) →
      AddContent.mk (C := C) toFun empty' sUnion' = AddContent.mk (C := C) toFun_1 empty'_1 sUnion'_1
⊢ AddContent.mk (C := C) toFun empty' sUnion' = m'

Tactic:
cases m'
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
toFun : Set α → G
empty' : toFun ∅ = 0
sUnion' :
  ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun u
toFun_1 : Set α → G
empty'_1 : toFun_1 ∅ = 0
sUnion'_1 :
  ∀ (I : Finset (Set α)) (_h_ss : (↑I : Set (Set α)) ⊆ C) (_h_dis : (↑I : Set (Set α)).PairwiseDisjoint id)
    (_h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C), toFun_1 (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, toFun_1 u
h :
  Eq (α := (a : Set α) → G)
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun empty' sUnion'))
    ((fun (m : AddContent G C) (s : Set α) ↦ m.toFun (C := C) s) (AddContent.mk (C := C) toFun_1 empty'_1 sUnion'_1))
⊢ AddContent.mk (C := C) toFun empty' sUnion' = AddContent.mk (C := C) toFun_1 empty'_1 sUnion'_1

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m m' : AddContent G C
h : ∀ (s : Set α), Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) s : G) ((m' : (a : Set α) → G) s : G)
⊢ m = m'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) ∅ : G) (0 : G)

Tactic:
m.empty'

Premises used: MeasureTheory.AddContent.empty'
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
I : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
h_ss : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
h_mem : ⋃₀ (↑I : Set (Set α)) ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃₀ (↑I : Set (Set α))) : G) (∑ u ∈ I, (m : (a : Set α) → G) u : G)

Tactic:
m.sUnion' I h_ss h_dis h_mem

Premises used: MeasureTheory.AddContent.sUnion'
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
⊢ ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
⊢ ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))

Tactic:
have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
rw : Eq.{u_2 + 1} (α := G) (∑ u ∈ Finset.image f a, (m : (a : Set α) → G) u) (∑ i ∈ a, (m : (a : Set α) → G) (f i))
h_ss : (↑(Finset.image f a) : Set (Set α)) ⊆ C
h_dis₁ : (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id
h_mem₁ : ⋃₀ (↑(Finset.image f a) : Set (Set α)) ∈ C
⊢ Eq.{u_2 + 1} (α := G) ((m : (a : Set α) → G) (⋃ i ∈ a, f i) : G) (∑ i ∈ a, (m : (a : Set α) → G) (f i) : G)

Tactic:
rw [A, addContent_sUnion]

Premises used: MeasureTheory.addContent_sUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ (↑(Finset.image f a) : Set (Set α)) ⊆ C

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a : Set ι).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ (↑(Finset.image f a) : Set (Set α))
⊢ (↑(Finset.image f a) : Set (Set α)).PairwiseDisjoint id

Tactic:
simpa using h_dis.image

Premises used: Set.Pairwise.image