mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
s : Set α
⊢ UpperSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
by
  simp [semicontinuousOn_iff_frequently]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
x : α
⊢ f x = g x → ∀ (y : Set β), IsOpen[inst✝] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst✝] y ∧ (g x ∩ y).Nonempty

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
x : α
hx : f x = g x
⊢ ∀ (y : Set β), IsOpen[inst✝] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst✝] y ∧ (g x ∩ y).Nonempty
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : UpperHemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
x : α
⊢ f x = g x → ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : UpperHemicontinuousWithinAt f s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, f x = g x
x : α
hx : f x = g x
⊢ ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : a ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

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

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

Tactic:
by
  rw [mul_comm, div_mul_cancel h₁ h₂ h₃]

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

Goal state before:
pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
obtain ⟨a', ha', aa'⟩ := exists_between ((div_lt_iff b0 b_top).2 h)

Goal state after:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
a' : EReal
ha' : c / b < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Tactic:
edist_comm

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f N) (f n) < ↑ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
⊢ x ∈ s → SemicontinuousWithinAt (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) s x

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst✝ : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn (fun y ↦ f y x) I (M x)
x : α
hx : x ∈ s
⊢ SemicontinuousWithinAt (fun x1 x2 ↦ (fun x ↦ f (M x) x) x1 > x2) s x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
x : EReal
⊢ x < ⊤ → ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ

Tactic:
hx

Goal state after:
case h
x : EReal
hx : x < ⊤
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici x ∩ {⊤}ᶜ
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inr.inr
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
rw [mul_top_of_pos a0] at hc; exact (not_top_lt hc).rec

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
x : EReal
⊢ ⊥ < x → ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
hx

Goal state after:
case h
x : EReal
hx : ⊥ < x
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Semiring 𝕜
inst✝² : Algebra ℚ≥0 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ 0 = (algebraMap ℚ≥0 𝕜) 0

Tactic:
map_zero

Goal state after:
𝕜 : Type u_4
inst✝³ : Semiring 𝕜
inst✝² : Algebra ℚ≥0 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ 0 = 0
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
have ⟨y', hy', z, hz, h₁⟩ := (h hx).exists_disjoint_Iio_Ioi

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
y' : γ
hy' : y' > (x, y).2
z : γ
hz : z < f (x, y).1
h₁ : ∀ x < y', ∀ y > z, x < y
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
A : Type u_5
inst✝⁷ : Semifield 𝕜
inst✝⁶ : CharZero 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousSMul ℚ≥0 𝕜
inst✝³ : Semiring A
inst✝² : Algebra 𝕜 A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul 𝕜 A
⊢ 0 = (algebraMap 𝕜 A) 0

Tactic:
map_zero

Goal state after:
𝕜 : Type u_4
A : Type u_5
inst✝⁷ : Semifield 𝕜
inst✝⁶ : CharZero 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousSMul ℚ≥0 𝕜
inst✝³ : Semiring A
inst✝² : Algebra 𝕜 A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul 𝕜 A
⊢ 0 = 0
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
⊢ h ≠ 0 → (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) h = (fun k ↦ (a + c * ↑k) / (b + d * ↑k)) h

Tactic:
hx

Goal state after:
case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) h = (fun k ↦ (a + c * ↑k) / (b + d * ↑k)) h
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
⊢ x ∈ g ⁻¹' {0}ᶜ → f x / g x * g x = f x

Tactic:
hx

Goal state after:
α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
x : α
hx : x ∈ g ⁻¹' {0}ᶜ
⊢ f x / g x * g x = f x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun x ↦ g x / f x) l (𝓝 a⁻¹)

Tactic:
by
    simp_rw [← inv_div (f _)]
    exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim

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

Goal state before:
pp: m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable fun i ↦ 1 / m ^ f i

Tactic:
by
  refine .of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
      (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
        ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
  rw [div_pow, one_pow]
  refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a)) <;>
    exact pow_pos (zero_lt_one.trans hm) _

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

Goal state before:
pp: case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
⊢ x ∈ Finset.range k → 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

Tactic:
hx

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
⊢ x ∈ Finset.range k → (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
hx

Goal state after:
case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe.bot
a✝ : ℝ
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
h₁ : ¬a✝ = 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

Tactic:
exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x = i
⊢ (fun x ↦ s) x ∈ π x

Tactic:
hx

Goal state after:
case refine_2.inl.refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x = i
⊢ (fun x ↦ s) i ∈ π i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m

Tactic:
refine generateFrom_le ?_
  rintro t ⟨ht_p, _, ft, hft_mem_pi, rfl⟩
  refine Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_
  exact measurableSet_generateFrom (hft_mem_pi x hx_mem)

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : SupSet β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
x : α
⊢ (∀ (i : ι), aeSeq hf p i x = f i x) → (⨆ n, aeSeq hf p n) x = (⨆ n, f n) x

Tactic:
hx

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : SupSet β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
x : α
hx : ∀ (i : ι), aeSeq hf p i x = f i x
⊢ (⨆ n, aeSeq hf p n) x = (⨆ n, f n) x
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
⊢ p ∈ ∅

Tactic:
fin_cases p

Goal state after:
case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated.3664957871._hygCtx._hyg.200.«0»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : True ∈ x
⊢ True ∈ ∅

case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated.3664957871._hygCtx._hyg.200.«1»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : False ∈ x
⊢ False ∈ ∅
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

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

Tactic:
have : ∀ n : ℕ, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (n : ℝ≥0∞)⁻¹ := by
      intro n
      refine this _ (ENNReal.lt_add_right hs ?_)
      simp

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
this : ∀ (n : ℕ), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
⊢ MeasurableEmbedding f

Tactic:
by
  set e : α ≃ᵐ range f :=
    ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective rangeFactorization_surjective⟩,
      hf₁.subtype_mk, hg⟩
  exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
⊢ map f 0 = 0

Tactic:
by_cases hf : AEMeasurable f (0 : Measure α)

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f 0
⊢ map f 0 = 0

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬AEMeasurable f 0
⊢ map f 0 = 0
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
⊢ s ⊆ t

Tactic:
subset_union_compl_iff_inter_subset,

Goal state after:
α : 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
⊢ s ∩ range f ⊆ f '' toMeasurable μ (f ⁻¹' s)
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
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ (map f μ) t = μ (f ⁻¹' s)

Tactic:
map_apply hf.measurable htm,

Goal state after:
α : 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
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : (map f ν) t = 0
⊢ (map f μ) t = 0

Tactic:
hf.map_apply

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
t : Set β
ht : ν (f ⁻¹' t) = 0
⊢ μ (f ⁻¹' t) = 0
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ ((comapₗ f) μ) s = μ (f '' s)

Tactic:
by
  rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure]
  exact ⟨hfi, hf⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)

Tactic:
refine le_antisymm ?_ (iSup_le fun i ↦ measure_mono <| subset_iUnion _ _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
⊢ x ∈ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i → x ∈ ∅

Tactic:
hx

Goal state after:
X : Type u_5
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
decr : Antitone fun n ↦ ⋃ i, ⋃ (_ : i ≥ n), Es i
x : X
hx : x ∈ ⋂ n, ⋃ i, ⋃ (_ : i ≥ n), Es i
⊢ x ∈ ∅
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ μ (⋂ i, f i) = μ (⋂ i, ⋂ j, ⋂ (_ : j ≤ i), f j)

Tactic:
iInter_comm

Goal state after:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ μ (⋂ i, f i) = μ (⋂ i', ⋂ i, ⋂ (_ : i' ≤ i), f i')
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
⊢ map f (μ.restrict s) ≪ ν.restrict t

Tactic:
refine AbsolutelyContinuous.mk fun u hum ↦ ?_
    suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]
    refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)
    rw [preimage_inter]
    gcongr
    assumption

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

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
⊢ x ∈ s → ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
hx

Goal state after:
case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos.hs
α : 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
this : atBot.IsCountablyGenerated
⊢ ∀ (i : { x // x ∈ Ioi a }), NullMeasurableSet (s ↑i) μ

pp: case pos.hm
α : 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
this : atBot.IsCountablyGenerated
⊢ Monotone fun x ↦ s ↑x

pp: case pos.hf
α : 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
this : atBot.IsCountablyGenerated
⊢ ∃ i, μ (s ↑i) ≠ ∞

Tactic:
· rwa [Subtype.forall]

Goal state after:
case pos.hm
α : 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
this : atBot.IsCountablyGenerated
⊢ Monotone fun x ↦ s ↑x

case pos.hf
α : 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
this : atBot.IsCountablyGenerated
⊢ ∃ i, μ (s ↑i) ≠ ∞
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 μ

pp: case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ

Tactic:
· infer_instance

Goal state after:
case mpr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : CompactSpace α
a✝ : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)

Tactic:
have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) := by
    let w n := toMeasurable (m n) t
    have T : t ⊆ ⋂ n, w n := subset_iInter (fun i ↦ subset_toMeasurable (m i) t)
    have M : MeasurableSet (⋂ n, w n) :=
      MeasurableSet.iInter (fun i ↦ measurableSet_toMeasurable (m i) t)
    refine ⟨⋂ n, w n, T, M, fun u hu ↦ ?_⟩
    refine le_antisymm ?_ (by gcongr)
    rw [hμ, sum_apply _ (M.inter hu)]
    apply le_trans _ (le_sum_apply _ _)
    apply ENNReal.tsum_le_tsum (fun i ↦ ?_)
    calc
    m i ((⋂ n, w n) ∩ u) ≤ m i (w i ∩ u) := by gcongr; apply iInter_subset
    _ = m i (t ∩ u) := measure_toMeasurable_inter hu (hv i)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
⊢ μ (toMeasurable μ t ∩ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : 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)
x : α
⊢ x ∈ t → x ∈ ⋃ i, t ∩ w i

Tactic:
hx

Goal state after:
α : 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)
x : α
hx : x ∈ t
⊢ x ∈ ⋃ i, t ∩ w i
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
x : α
⊢ x ∈ t → s x ≤ (t ∩ s) x

Tactic:
hx

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
x : α
hx : x ∈ t
⊢ s x ≤ (t ∩ s) x