mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
E₁ : ι → Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedField 𝕜
inst✝¹⁵ : (i : ι) → TopologicalSpace (E i)
inst✝¹⁴ : (i : ι) → AddCommGroup (E i)
inst✝¹³ : (i : ι) → Module 𝕜 (E i)
inst✝¹² : (i : ι) → TopologicalSpace (E₁ i)
inst✝¹¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝¹⁰ : (i : ι) → Module 𝕜 (E₁ i)
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
g : F ≃L[𝕜] G
x✝ : ContinuousMultilinearMap 𝕜 E G
⊢ (↑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E F G) ↑g)).toFun
      (((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 E G F) ↑g.symm) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝ : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsCompl p q
⊢ IsTopCompl p q ↔ Continuous[inst✝², instTopologicalSpaceSubtype] ⇑(p.projectionOnto q h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : ContinuousSub M
h : IsTopCompl p q
⊢ Continuous[inst✝³, inst✝³] ⇑(q.projection p ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsTopCompl ⊥ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsTopCompl ⊤ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
N : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace N
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse ⇑f₂ ⇑f₁
p : N →L[R] N := f₁ ∘SL f₂
⊢ IsIdempotentElem p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsTopCompl p (↑f).ker

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsTopCompl p q
⊢ (↑(p.projectionOntoL q h)).range = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsTopCompl p q
⊢ (↑(p.projectionOntoL q h)).ker = q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsTopCompl p q
⊢ (↑(p.projectionL q h)).range = p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsTopCompl p q
⊢ (↑(p.projectionL q h)).ker = q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : IsTopCompl p q
⊢ IsIdempotentElem (p.projectionL q h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : ContinuousSub M
h : IsTopCompl p q
x : M
⊢ (q.projectionL p ⋯) x = x - (p.projectionL q h) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : T1Space ↥p
h : IsTopCompl p q
⊢ IsClosed[inst✝³] ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsTopCompl p q
hq : IsClosed[inst✝³] ↑q
⊢ IsClosed[instTopologicalSpaceSubtype] {0}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsTopCompl p q
hq : IsClosed[inst✝³] ↑q
⊢ T3Space ↥p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (x✝, 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (0, x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsTopCompl p q ↔ IsHomeomorph ⇑(p.prodEquivOfIsCompl q h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype] ⇑(p.quotientEquivOfIsCompl q h)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
⊢ ofIsTopCompl h φ ψ = φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
x : ↥p
⊢ (ofIsTopCompl h φ ψ) ↑x = φ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
x : ↥q
⊢ (ofIsTopCompl h φ ψ) ↑x = ψ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
χ : E →L[R] F
hφ : ∀ (u : ↥p), φ u = χ ↑u
hψ : ∀ (u : ↥q), ψ u = χ ↑u
⊢ ofIsTopCompl h φ ψ = χ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
⊢ ofIsTopCompl h 0 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ₁ φ₂ : ↥p →L[R] F
ψ₁ ψ₂ : ↥q →L[R] F
⊢ ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁸ : Ring R
E : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : Module R F
inst✝ : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ↥p →L[R] F
ψ : ↥q →L[R] F
⊢ (↑(ofIsTopCompl h φ ψ)).range = (↑φ).range ⊔ (↑ψ).range

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.real s = 0 ↔ μ s = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.real s ≠ 0 ↔ μ s ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
⊢ μ.real ∅ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
⊢ μ univ ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ ENNReal.ofReal (μ.real s) = μ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ (c • μ).real s = c.toReal * μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0
⊢ (c • μ).real s = ↑c * μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : MeasurableSet s
⊢ (map f μ).real s = μ.real (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
m : MeasurableSpace β
ν : Measure β
t : Set β
h₁ : μ s ≠ ∞
h₂ : ν t ≠ ∞
⊢ μ.real s = ν.real t ↔ μ s = ν t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t (μ.restrict s)
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s).real univ = μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).real t = μ.real (t ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s).real s = μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : μ.real s₂ = 0
h'₂ : μ s₂ ≠ ∞
⊢ μ.real s₁ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ t ≠ ∞
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ s ≠ ∞
⊢ μ.real t ≤ μ.real (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ (s₁ ∪ s₂) < ∞
A : μ s₁ ≠ ∞
B : μ s₂ ≠ ∞
⊢ μ s₁ + μ s₂ ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
f : β → Set α
a✝ : β
s✝ : Finset β
hx : a✝ ∉ s✝
IH : μ.real (⋃ b ∈ s✝, f b) ≤ ∑ p ∈ s✝, μ.real (f p)
⊢ μ.real (f a✝) + μ.real (⋃ x ∈ s✝, f x) ≤ μ.real (f a✝) + ∑ p ∈ s✝, μ.real (f p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → Set α
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : Fintype β
f : β → Set α
⊢ μ.real (⋃ b, f b) ≤ ∑ p, μ.real (f p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : ∀ (i : β), μ (f i) ≠ ∞
⊢ μ.real (⋃ b, f b) = ∑ p, μ.real (f p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real s₁ + μ.real s₂ ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h₁ : μ s₁ ≠ ∞
h₂ : μ s₂ ≠ ∞
h : μ.real (s₁ ∪ s₂) = 0
⊢ μ (s₁ ∪ s₂) ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
H : s =ᵐ[μ] t
⊢ μ.real s = μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) = μ.real s + μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) = μ.real s + μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
⊢ μ.real s + μ.real sᶜ = μ.real univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∆ t) = μ.real (s \ t) + μ.real (t \ s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u < ∞
⊢ μ (s ∆ t) ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
hu : μ u < ∞
⊢ μ (t ∆ u) ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
h : ∀ b ∈ s, μ (f b) ≠ ∞
⊢ μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
s : Finset β
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
h : ∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ∞
⊢ ∑ b ∈ s, μ.real (f ⁻¹' {b}) = μ.real (f ⁻¹' ↑s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSingletonClass α
inst✝ : SigmaFinite μ
s : Finset α
⊢ ∑ b ∈ s, μ.real {b} = μ.real ↑s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : μ s₁ ≠ ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : μ s₂ ≠ ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real s + μ.real (t \ s) = μ.real (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hm : MeasurableSet t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s \ t) = μ.real (s ∪ t) - μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h₁ : μ s₁ ≠ ∞
⊢ μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ s₂ ≠ ∞
⊢ μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : μ t ≠ ∞
⊢ μ.real (t \ s) < ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
ht' : μ t ≠ ∞
⊢ μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hst : s ⊆ t
h_nulldiff : μ.real (t \ s) = 0
h : μ (t \ s) ≠ ∞
⊢ μ.real s = μ.real t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : μ (s₃ \ s₁) ≠ ∞
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real sᶜ = μ.real univ - μ.real s

Tactic:
by

Goal state after: