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

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

Tactic:
filter_upwards [hfg] with x hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Preorder β
f g : α → β
s : Set α
a : α
h : LowerSemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
x : α
hx : f x = g x
⊢ ∀ (y : β), f x > y ↔ g x > y
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 : α) in 𝓝[s] a, ∀ (y : Set β), IsOpen[inst✝] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst✝] y ∧ (g x ∩ y).Nonempty

Tactic:
filter_upwards [hfg] with x 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 : α) in 𝓝[s] a, ∀ (y : Set β), y ∈ 𝓝ˢ (f x) ↔ y ∈ 𝓝ˢ (g x)

Tactic:
filter_upwards [hfg] with x 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: case coe
a : ℝ
h : ↑a ≤ 0
⊢ a⁻¹ ≤ 0

Tactic:
inv_nonpos

Goal state after:
case coe
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
obtain ⟨a, ha, h⟩ := hs hℱs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
this : ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
⊢ False

Tactic:
by rwa [eventually_const] at this

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case inr
α : Type u_4
s : Set α
hinf : s.Infinite
⊢ ∑' (x : ↑s), 1 = ↑s.encard

Tactic:
· have : Infinite s := infinite_coe_iff.mpr hinf
    rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

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

Goal state before:
pp: a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ ↑(2 * max (x + 1) 0 / a)

Tactic:
rw [EReal.coe_nonneg]

Goal state after:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ 2 * max (x + 1) 0 / a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ ↑(δ' i) / ↑(max 1 (w i)) ≤ ↑(δ' i) / (fun i ↦ ↑(w i)) i

Tactic:
← le_max_right

Goal state after:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ ↑(δ' i) / ↑(w i) ≤ ↑(δ' i) / (fun i ↦ ↑(w i)) i
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b, g b)
⊢ ∃ T f, t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
by
  classical
  induction h_t with
  | @base s h_s =>
    rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
    refine ⟨{b}, fun _ => s, ?_⟩
    simpa using h_s_in_t'
  | inter h_gen_s h_gen_t' h_nonempty h_s h_t' =>
    rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
    rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
    use T_s ∪ T_t', fun b : β =>
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b
      else if b ∈ T_t' then f_t' b else (∅ : Set α)
    constructor
    · ext a
      simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union]
      grind
    intro b h_b
    split_ifs with hbs hbt hbt
    · refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)
      exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
    · exact h_s b hbs
    · exact h_t' b hbt
    · rw [Finset.mem_union] at h_b
      apply False.elim (h_b.elim hbs hbt)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ ∃ t, ∃ (_ : ↑t ⊆ S), ∃ f, ∃ (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x

Tactic:
use p1 ∪ p2, hp_union_ss, g

Goal state after:
case h
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := ⋯
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = univ

Tactic:
use Set.univ

Goal state after:
case h
α : Type u_1
s : Set α
⊢ (fun x ↦ x ∈ s) ⁻¹' univ = univ
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ extend m (disjointed f i) ≤ extend m (f i)

Tactic:
exact extend_mono m0 mU (MeasurableSet.disjointed h _) (disjointed_le f _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set β
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)

Tactic:
rw [← image_preimage_eq_inter_range, hf.measurableSet_image]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).domRestrict (extend f g g'))

Tactic:
rw [domRestrict_extend_range]
    simpa only [rangeSplitting] using! hg.comp hf.measurable_rangeSplitting

Goal state after:
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 γ
⊢ Measurable ⇑(Equiv.prodAssoc α β γ)

Tactic:
eta_expand

Goal state after:
α : 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 γ
⊢ Measurable fun a ↦ (Equiv.prodAssoc α β γ) a
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 γ
⊢ Measurable ⇑(Equiv.prodAssoc α β γ).symm

Tactic:
eta_expand

Goal state after:
α : 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 γ
⊢ Measurable fun a ↦ (Equiv.prodAssoc α β γ).symm a
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 γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable ⇑(Equiv.sumPiEquivProdPi α)

Tactic:
eta_expand

Goal state after:
α✝ : 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 γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ Measurable fun a ↦ (Equiv.sumPiEquivProdPi fun a ↦ α a) fun i ↦ a i
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ Measurable f

Tactic:
by rw [← hf.2.1]; exact comap_measurable f

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t, (∀ (i : ι), MeasurableSet (t i)) ∧ (∀ (i : ι), μ (t i) = 0) ∧ Pairwise (Disjoint on fun i ↦ s i \ t i)

Tactic:
by
  refine ⟨fun i => toMeasurable μ (s i ∩ ⋃ j ∈ ({i}ᶜ : Set ι), s j), fun i =>
    measurableSet_toMeasurable _ _, fun i => ?_, ?_⟩
  · simp only [measure_toMeasurable, inter_iUnion]
    exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)
  · simp only [Pairwise, disjoint_left, onFun, mem_sdiff, not_and, and_imp, Classical.not_not]
    intro i j hne x hi hU hj
    replace hU : x ∉ s i ∩ iUnion fun j ↦ iUnion fun _ ↦ s j :=
      fun h ↦ hU (subset_toMeasurable _ _ h)
    simp only [mem_inter_iff, mem_iUnion, not_and, not_exists] at hU
    exact (hU hi j hne.symm hj).elim

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

Goal state before:
pp: case refine_1.succ
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet ((F ∘ F^[n]) univ)

Tactic:
Function.comp_apply

Goal state after:
case refine_1.succ
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F (F^[n] univ))
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2.a.succ
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ (F ∘ F^[n✝]) univ

Tactic:
Function.comp_apply

Goal state after:
case refine_2.a.succ
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F (F^[n✝] univ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ (F ∘ F^[n]) univ
⊢ y ∈ f '' F^[n] univ

Tactic:
Function.comp_apply

Goal state after:
case a
α : 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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
⊢ y ∈ f '' F^[n] univ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ∞
ε : ℝ≥0∞
⊢ μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε

Tactic:
by
  rw [measure_sdiff hst hs hs', tsub_le_iff_left]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
f : ι → Set α
⊢ μ (⋃ x, accumulate f x) = ⨆ i, μ (accumulate f i)

Tactic:
exact monotone_accumulate.measure_iUnion

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, μ (s ∩ t) = 0
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : ⋃ n, t n = univ
⊢ μ s = 0

Tactic:
rw [show s = ⋃ n, s ∩ t n by rw [← inter_iUnion, ht2, inter_univ], measure_iUnion_null_iff]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
C : Set (Set α)
ht : ∀ t ∈ C, μ (s ∩ t) = 0
t : ℕ → Set α
ht1 : ∀ (n : ℕ), t n ∈ C
ht2 : ⋃ n, t n = univ
⊢ ∀ (i : ℕ), μ (s ∩ t i) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ |(μ (s \ t)).toReal - (μ (t \ s)).toReal| ≤ (μ (s \ t)).toReal + (μ (t \ s)).toReal

Tactic:
convert! abs_sub (μ (s \ t)).toReal (μ (t \ s)).toReal

Goal state after:
case e'_4.e'_5
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ (μ (s \ t)).toReal = |(μ (s \ t)).toReal|

case e'_4.e'_6
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
this : (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal
⊢ (μ (t \ s)).toReal = |(μ (t \ s)).toReal|
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case iUnion
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
f : ℕ → Set ↑s
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val '' f n) μ
⊢ NullMeasurableSet (Subtype.val '' ⋃ i, f i) μ

Tactic:
rw [image_iUnion]
    exact .iUnion hf

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

Goal state before:
pp: δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume univ = volume u

Tactic:
rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]

Goal state after:
δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ volume (Subtype.val '' univ) = volume u

δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Injective Subtype.val

δ : Type u_4
u : Set δ
inst✝ : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ ∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
q : ℕ → (ℕ → Prop) → Prop
hq : ∀ (n : ℕ), t n = ⋃ p, if q n p then countablyGeneratedAtom α p else ∅
⊢ ∃ q, ⋃ i, t i = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
refine ⟨fun p ↦ ⨆ n, q n p, ?_⟩

Goal state after:
case refine_4
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
q : ℕ → (ℕ → Prop) → Prop
hq : ∀ (n : ℕ), t n = ⋃ p, if q n p then countablyGeneratedAtom α p else ∅
⊢ ⋃ i, t i = ⋃ p, if (fun p ↦ ⨆ n, q n p) p then countablyGeneratedAtom α p else ∅
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

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

Tactic:
constructor
  · intro h
    exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)
  · intro h
    refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩
    have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
    have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
    exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
M : ∀ (i : ι), AEMeasurable f (m i)
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Tactic:
simp_rw [map_apply_of_aemeasurable (M _) hs]

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ (⋂ i ∈ s, {i}ᶜ)

Tactic:
exact .biInter hs fun x _ => .compl_singleton x

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

Goal state before:
pp: case mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
y : α
hy : y < a
l : α
hlt : l ∈ t
hly : l ≤ y
u : α
hut : u ∈ t
hyu : y < u
hua : u < a
⊢ ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 ≤ a), i ≤ y ∧ y < i_1

Tactic:
exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua.le, hly, hyu⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t

Tactic:
cthickening,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ {x | infEDist x (s ∪ t) ≤ ENNReal.ofReal δ} =
    {x | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x | infEDist x t ≤ ENNReal.ofReal δ}
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
⊢ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = cthickening δ s

Tactic:
cthickening,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
⊢ {x | infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ ENNReal.ofReal δ} =
    {x | infEDist x s ≤ ENNReal.ofReal δ}
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Prod.instMeasurableSpace ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
refine sup_le ?_ ?_ <;> rw [comap_generateFrom]

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.fst '' C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.snd '' D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)