mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ c * a / b = a * c / b

Tactic:
mul_comm

Goal state after:
a b c : EReal
⊢ a * c / b = a * c / b
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a * c / (b * c) = a / b

Tactic:
rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -(b⁻¹ * a) ≤ -(a' * b⁻¹)

Tactic:
mul_comm a' b⁻¹,

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ -(b⁻¹ * a) ≤ -(b⁻¹ * a')
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ⊤) ↔ Tendsto f l atTop

Tactic:
rw [tendsto_nhds_top_iff_real, atTop_basis_Ioi.tendsto_right_iff]

Goal state after:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := ⋯
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
i : ℕ
⊢ ∀ (i_1 : ℕ), f i i_1 ⊆ ⋃ i, f (Nat.pairEquiv.symm i).1 (Nat.pairEquiv.symm i).2

Tactic:
simp only [Nat.pairEquiv_symm_apply]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
f : ℕ → ℕ → Set α
hf : ∀ (i : ℕ), s i ⊆ ⋃ i_1, f i i_1 ∧ ∑' (i_1 : ℕ), m (f i i_1) < μ (s i) + ↑(ε' i)
i : ℕ
⊢ ∀ (i_1 : ℕ), f i i_1 ⊆ ⋃ i, f (Nat.unpair i).1 (Nat.unpair i).2
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
by_cases hx₁ : ∃ l, l < f x

Goal state after:
case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun x ↦ (↑x)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atTop_nhds_zero_nat

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this✝ : r ≠ 1
this : Tendsto (fun n ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)

Tactic:
by
    simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * (C * 2⁻¹ ^ n)

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ C * 2⁻¹ ^ n * 2
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))

Tactic:
refine HasSum.mul_left C ?_

Goal state after:
case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (HPow.hPow r) (1 - r)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst✝¹] (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Ici y)

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Ici]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 : Set α
ht1 : ∃ i, t1 ∈ p i
t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
⊢ ∃ i, t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨n, ht1⟩ := ht1

Goal state after:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
⊢ ∃ i, t1 ∩ t2 ∈ p i
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ (s₁ ∪ s₂) ∩ s₁) + m (t ∩ ((s₁ ∪ s₂) \ s₁)) + m (t \ (s₁ ∪ s₂))

Tactic:
Set.inter_assoc _ _ s₁,

Goal state after:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ ((s₁ ∪ s₂) ∩ s₁)) + m (t ∩ ((s₁ ∪ s₂) \ s₁)) + m (t \ (s₁ ∪ s₂))
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ ∀ (i : P s), m s h ≤ m s i

Tactic:
intro

Goal state after:
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h i✝ : P s
⊢ m s h ≤ m s i✝
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
ι : Sort u_4
p : α → ι → Prop
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i
i : ι
⊢ ∀ᵐ (a : α) ∂μ, p a i

Tactic:
by
  filter_upwards [hp] with a ha using ha i

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
this : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
rcases this with ⟨t, hmt, hin, hlt⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
t : Set α
hmt : MeasurableSet t
hin : s ⊆ t
hlt : m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⇑(Equiv.Set.rangeInr α β) ⁻¹' s)

Tactic:
refine ⟨_, hs.inr_image, Set.ext ?_⟩
    simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
⊢ f '' f ⁻¹' s ⊆ f '' toMeasurable μ (f ⁻¹' s)

Tactic:
exact image_mono (subset_toMeasurable _ _)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν' : Measure α
h : μ ≪ ν'
ν : Measure α
⊢ μ ≪ ν + ν'

Tactic:
by
  simp [add_comm, add_right h]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (m i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝ : IsEmpty α
⊢ IsFiniteMeasure 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝ : SigmaFinite μ
this : ∀ (n : ℕ), Fact (μ (disjointed (spanningSets μ) n) < ∞)
n : ℕ
⊢ IsFiniteMeasure ((fun n ↦ μ.restrict (disjointed (spanningSets μ) n)) n)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
R : Type u_5
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsFiniteMeasure μ
r : R
⊢ IsFiniteMeasure ((r • 1) • μ)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
hC : IsCountablySpanning C
ht : ∀ t ∈ C, μ (s ∩ t) = 0
⊢ μ s = 0

Tactic:
by
  obtain ⟨t, ht1, ht2⟩ := hC
  rw [show s = ⋃ n, s ∩ t n by rw [← inter_iUnion, ht2, inter_univ], measure_iUnion_null_iff]
  exact fun i => ht (t i) (ht1 i)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
δ : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
⊢ ⋃ i, f ⁻¹' Metric.ball x ↑i = univ

Tactic:
by rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : Order.IsPredPrelimit a
⊢ (comap Subtype.val (𝓝[>] a)).IsCountablyGenerated

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case mp
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasureOnCompacts μ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n ∩ u) = (μ.restrict (t ∩ u)) (disjointed w n)

Tactic:
rw [restrict_apply, inter_comm t _, inter_assoc]

Goal state after:
case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ MeasurableSet (disjointed w n)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case e_f
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n✝ n : ℕ
⊢ MeasurableSet (w n)

Tactic:
exact measurableSet_toMeasurable _ _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
i n : ℕ
⊢ MeasurableSet (w n)

Tactic:
exact measurableSet_toMeasurable _ _

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

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume

Tactic:
exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : IsEmpty α
⊢ SigmaFinite 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
⊢ (∃ i, i n ∧ x ∈ countablyGeneratedAtom α i) → x ∈ natGeneratingSequence α n

Tactic:
· rintro ⟨p, hpn, hpx⟩
      simp only [countablyGeneratedAtom, mem_iInter] at hpx
      specialize hpx n
      simpa [hpn] using hpx

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
μ : Measure α
h : IsFiniteMeasure μ
⊢ SigmaFinite μ

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x

Tactic:
by
  rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → β
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
⊢ s.piecewise f g =ᵐ[μ.restrict sᶜ] g

Tactic:
rw [ae_restrict_eq hs.compl]
  exact (piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ generateFrom (⋃ n, memPartition t n) ≤ m

Tactic:
by
  refine (generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)
  rintro s ⟨i, rfl⟩
  exact ht i

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : CountablyGenerated γ
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable α
⊢ CountableOrCountablyGenerated α γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty β
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated α γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable β
⊢ CountableOrCountablyGenerated β γ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated β γ

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
⊢ AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)

Tactic:
by
  rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ✝ ν μ : Measure α
f : α → β
inst✝ : SFinite μ
H : AEMeasurable f (sum (sfiniteSeq μ))
⊢ SFinite (sum fun i ↦ map f (sfiniteSeq μ i))

Tactic:
infer_instance

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ✝ ν μ : Measure α
f : α → β
inst✝ : SFinite μ
H : ¬AEMeasurable f μ
⊢ SFinite 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹⁵ : TopologicalSpace α✝
inst✝¹⁴ : MeasurableSpace α✝
inst✝¹³ : OpensMeasurableSpace α✝
inst✝¹² : TopologicalSpace β✝
inst✝¹¹ : MeasurableSpace β✝
inst✝¹⁰ : OpensMeasurableSpace β✝
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
inst✝¹⁵ : TopologicalSpace α✝
inst✝¹⁴ : MeasurableSpace α✝
inst✝¹³ : OpensMeasurableSpace α✝
inst✝¹² : TopologicalSpace β✝
inst✝¹¹ : MeasurableSpace β✝
inst✝¹⁰ : OpensMeasurableSpace β✝
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
⊢ SecondCountableTopology β

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SecondCountableTopology α

Tactic:
infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝¹ : Preorder α
a b x : α
μ : Measure α
inst✝ : OrderClosedTopology α
⊢ (𝓝[Ici a] x ⊓ 𝓝[Iic b] x).IsMeasurablyGenerated

Tactic:
infer_instance

Goal state after: