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

Goal state before:
pp: b : EReal
h : b < 0
h' : b ≠ ⊥
⊢ StrictAnti fun a ↦ a / b

Tactic:
intro a a' a_lt_a'
  simp only
  apply lt_of_le_of_ne <| div_le_div_right_of_nonpos (le_of_lt h) (le_of_lt a_lt_a')
  intro hyp
  apply ne_of_lt a_lt_a'
  rw [← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
    @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]

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

Goal state before:
pp: ⊢ IsOpen (range Real.toEReal)

Tactic:
simp only [range_coe_eq_Ioo, isOpen_Ioo]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ ∑' (i : ℕ), m ((fun x ↦ ∅) i) ≤ 0

Tactic:
by simpa

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

Goal state before:
pp: ⊢ Continuous toENNReal

Tactic:
by
  refine continuous_iff_continuousAt.mpr fun x ↦ ?_
  by_cases h_top : x = ⊤
  · simp only [ContinuousAt, h_top, toENNReal_top]
    refine ENNReal.tendsto_nhds_top fun n ↦ ?_
    filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy
    exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy
  refine ContinuousOn.continuousAt ?_ (compl_singleton_mem_nhds_iff.mpr h_top)
  refine (continuousOn_of_forall_continuousAt fun x hx ↦ ?_).congr (fun _ h ↦ toENNReal_of_ne_top h)
  by_cases h_bot : x = ⊥
  · refine tendsto_nhds_of_eventually_eq ?_
    rw [h_bot, nhds_bot_basis.eventually_iff]
    simpa [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and] using
      ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩
  refine ENNReal.continuous_ofReal.continuousAt.comp' <| continuousOn_toReal.continuousAt
    <| (toFinite _).isClosed.compl_mem_nhds ?_
  simp_all only [mem_compl_iff, mem_singleton_iff, mem_insert_iff, or_self, not_false_eq_true]

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
this : Tendsto (fun n ↦ 1 / ↑(n + 1)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ 1 / (↑n + 1)) atTop (𝓝 0)

Tactic:
by simpa

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

Goal state before:
pp: r : ℝ≥0∞
hr : r < 1
ι : Type u_4
inst✝ : Encodable ι
⊢ ∑' (y : ℕ), r ^ y < ∞

Tactic:
by simpa

Goal state after:
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}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
A1 : min (f z) (f x) ∈ u
⊢ f z + g z > y

Tactic:
have : (min (f z) (f x), g x) ∈ u ×ˢ v := ⟨A1, xv⟩

Goal state after:
α : 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
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
h₁z : f z > z₁
A1 : min (f z) (f x) ∈ u
this : (min (f z) (f x), g x) ∈ u ×ˢ v
⊢ f z + g z > y
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ (⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)

Tactic:
rw [iInf, sInf_apply' hs]
  simp only [iInf_range]

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

Goal state before:
pp: ⊢ ∀ᶠ (b : ℕ) in atTop, ↑b ! / ↑b ^ b ≤ 1 / ↑b

Tactic:
refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_
      rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
      rw [factorial_eq_prod_range_add_one, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
        Finset.prod_range_succ']
      simp only [one_mul, Nat.cast_add, zero_add, Nat.cast_one]
      refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;>
          intro x hx <;>
        rw [Finset.mem_range] at hx
      · positivity
      · refine (div_le_one <| mod_cast hn).mpr ?_
        norm_cast
        lia

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 γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable ⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β)

Tactic:
dsimp [Equiv.arrowProdEquivProdArrow]
    fun_prop

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 γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable ⇑(Equiv.arrowProdEquivProdArrow γ (fun i ↦ α) fun i ↦ β).symm

Tactic:
dsimp [Equiv.arrowProdEquivProdArrow]
    fun_prop

Goal state after:
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)
e : α ≃ᵐ ↑(range f) :=
  { toFun := rangeFactorization f, invFun := g, left_inv := H, right_inv := ⋯, measurable_toFun := ⋯,
    measurable_invFun := hg }
⊢ MeasurableEmbedding f

Tactic:
exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding

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

Goal state before:
pp: case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s

Tactic:
have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]

Goal state after:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
this : toMeasurable μ (s \ t) =ᵐ[μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (fun x ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s

Tactic:
rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ map Subtype.val atBot = 𝓝[>] a

Tactic:
refine map_coe_atTop_of_Ioo_subset (s := ofDual ⁻¹' s) (b := toDual a) hsa ?_ ha.dual

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ ∀ a' < toDual a, ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : μ univ < ∑ i ∈ s, μ (t i)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Tactic:
by
  contrapose! H
  apply sum_measure_le_measure_univ h
  intro i hi j hj hij
  exact (disjoint_iff_inter_eq_empty.mpr (H i hi j hj hij)).aedisjoint

Goal state after:
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 ≠ ∞
⊢ |μ.real s - μ.real t| ≤ μ.real (s ∆ t)

Tactic:
simp only [Measure.real]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
⊢ |(μ s).toReal - (μ t).toReal| ≤ (μ (s ∆ t)).toReal
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t

Tactic:
simp only [restrict_apply, ht, inter_iUnion]

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) = ∑' (i : ι), μ (t ∩ s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : T1Space β
inst✝¹ : SecondCountableTopology β
inst✝ : Nonempty β
f : α → β
h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b
m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure
⊢ ∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)

Tactic:
replace h : ∀ b : β, m {b}ᶜ ≠ 0 := fun b => not_eventually.mpr (h b)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : T1Space β
inst✝¹ : SecondCountableTopology β
inst✝ : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure
h : ∀ (b : β), m {b}ᶜ ≠ 0
⊢ ∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos
α : 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
⊢ Tendsto ((⇑μ ∘ s) ∘ Subtype.val) atBot (𝓝 (μ (⋂ r ∈ Ioi a, s r)))

Tactic:
biInter_eq_iInter

Goal state after:
case pos
α : 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
⊢ Tendsto ((⇑μ ∘ s) ∘ Subtype.val) atBot (𝓝 (μ (⋂ x, s ↑x)))
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : ℕ → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] ⋃₀ D n
⊢ (⋃ n, D n).Countable

Tactic:
by simp [D_count]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case refine_2.inr
α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s✝ : Set α
h : HasCountableSeparatingOn α p s✝
hs : s✝ ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : ∀ s ∈ S, p s
hS : ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
x y : α
hx : (x ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → x ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → x ∉ i
hy : (y ∈ s✝ ∧ ∀ (t : Set α), t ∈ S ∧ t ∈ l.sets → y ∈ t) ∧ ∀ i ∈ S, iᶜ ∈ l → y ∉ i
s : Set α
hsS : s ∈ S
hsl : sᶜ ∈ l
⊢ x ∈ s ↔ y ∈ s

Tactic:
| inr hsl =>

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
k : ℕ
⊢ k ∈ {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} ↔ k ∈ univ

Tactic:
simp [le_or_gt]

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✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
s : α → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), μ (s x) < ∞
t : Set α
htc : t.Countable
htU : ⋃ x ∈ t, s x = univ
⊢ SigmaFinite μ

Tactic:
refine Measure.sigmaFinite_of_countable (htc.image s) (forall_mem_image.2 fun x _ => hsμ x) ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ ν : Measure α
s✝ t✝ : Set α
a : α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
s : α → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), μ (s x) < ∞
t : Set α
htc : t.Countable
htU : ⋃ x ∈ t, s x = univ
⊢ ⋃₀ (s '' t) = univ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ AEMeasurable f (sum μ)

Tactic:
set s : ι → Set α := fun i => toMeasurable (μ i) { x | f x ≠ (h i).mk f x }

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
⊢ AEMeasurable f (sum μ)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u ∈ memPartition t 0
⊢ MeasurableSet u

Tactic:
simp only [memPartition_zero, mem_singleton_iff] at hun

Goal state after:
case refine_1.zero
α : Type u_1
t : ℕ → Set α
u : Set α
hun : u = univ
⊢ MeasurableSet u
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:
refine (generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)
  rintro s ⟨i, rfl⟩
  exact ht i

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ ⋂₀ T

Tactic:
refine subset_sInter fun t tinT ↦ ?_

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t✝ : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t✝
t_cl : IsClosed[inst✝¹] t✝
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t✝ = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t✝ ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
t : Set X
tinT : t ∈ T
⊢ ⋂ i, closure[inst✝¹] (g' i) ⊆ t
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst✝¹] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst✝¹] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst✝¹] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst✝¹] (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure[inst✝¹] (g' i)
⊢ t ⊆ sᶜ

Tactic:
exact st_dis.subset_compl_left

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

Goal state before:
pp: case inter
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u s₁ s₂ : Set α
a✝¹ : GenerateOpen s s₁
a✝ : GenerateOpen s s₂
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
| inter s₁ s₂ _ _ hs₁ hs₂ =>

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < ↑ε / 2
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε

Tactic:
have : infEDist x (closure s) < infEDist x (closure s) + ε / 2 :=
    ENNReal.lt_add_right h.ne ε0.ne'

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < ↑ε / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε / 2
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ↑ε
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam s = ∞ → ediam (cthickening (↑ε) s) = ∞

pp: case refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ∞ → ediam (cthickening (↑ε) s) = ∞

pp: case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε

Tactic:
· exact fun h ↦ top_unique <| h ▸ ediam_mono (self_subset_cthickening _)

Goal state after:
case refine_2
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ∞ → ediam (cthickening (↑ε) s) = ∞

case refine_3
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * ↑ε).toReal = diam s + 2 * ↑ε
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
this : r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i
⊢ a ∈ {a | r a (f a)} ↔ a ∈ ⋃ b ∈ range ⇑f, {a | r a b} ∩ ⇑f ⁻¹' {b}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ≥0
hr : r₁ ≠ r₂
⊢ ENNReal.ofReal ↑r₁ ≠ ENNReal.ofReal ↑r₂

Tactic:
by simpa

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

Goal state before:
pp: x ε : ℝ
⊢ TotallyBounded (ball x ε)

Tactic:
rw [Real.ball_eq_Ioo]; apply totallyBounded_Ioo

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

Goal state before:
pp: case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
hx : x ∈ s ∩ f ⁻¹' {∞}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ∞
⊢ False

Tactic:
have : f x < ∞ := h'x.2.2

Goal state after:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
hx : x ∈ s ∩ f ⁻¹' {∞}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ∞
this : f x < ∞
⊢ False
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

Tactic:
have : f p = 0 := by
      contrapose! H
      rw [← Function.mem_support] at H
      exact fs (subset_tsupport _ H)
    simp [SimpleFunc.piecewise_apply, H, this, hε]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst✝ : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
⊢ (simpleFuncAux f g n.succ) (g m) = f (g m)

Tactic:
by
    obtain hnm | hnm := eq_or_ne (g n) (g m) <;>
      simp [simpleFuncAux, Set.piecewise_eq_of_notMem, hnm.symm, simpleFuncAux_eq_of_lt _ hmn]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
x : α
p_eq : ¬c (rs x) = 0
this✝¹ : r * s x ≠ 0
this✝ : s x ≠ 0
this : r * s x < 1 * s x
⊢ rs x < s x

Tactic:
by simpa

Goal state after: