mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)

Goal state after:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ 0 ≤ sign a ↔ 0 ≤ a

case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ 0 ≤ sign a ↔ 0 ≤ a

case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ sign a ↔ 0 ≤ a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)

Goal state after:
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ sign a ≤ 0 ↔ a ≤ 0

case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ sign a ≤ 0 ↔ a ≤ 0

case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ ↑(sign ↑x) * ↑(↑x).abs = ↑x

Tactic:
rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

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

Goal state before:
pp: x : EReal
x0 : 0 < x
a b : EReal
h : a ≤ b
⊢ (fun x y ↦ ↑x * y) ⟨x, x0⟩ a ≤ (fun x y ↦ ↑x * y) ⟨x, x0⟩ b

Tactic:
simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢

Goal state after:
x : EReal
x0 : 0 < x
a b : EReal
h :
  sign a < sign b ∨
    sign a = neg ∧ sign b = neg ∧ b.abs ≤ a.abs ∨
      sign a = zero ∧ sign b = zero ∨ sign a = pos ∧ sign b = pos ∧ a.abs ≤ b.abs
⊢ sign a < sign b ∨
    sign a = neg ∧ sign b = neg ∧ x.abs * b.abs ≤ x.abs * a.abs ∨
      sign a = zero ∧ sign b = zero ∨ sign a = pos ∧ sign b = pos ∧ x.abs * a.abs ≤ x.abs * b.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ↑a * ↑n ≤ ↑m

Tactic:
← coe_coe_eq_natCast n,

Goal state after:
case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ↑a * ↑↑n ≤ ↑m
Module: Mathlib.Topology.Semicontinuity.Defs

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

Tactic:
lowerHemicontinuousWithinAt_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 : α → Set β
x : α
⊢ LowerHemicontinuousWithinAt f univ x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
lowerHemicontinuousWithinAt_iff_frequently

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
rw [← lowerHemicontinuousWithinAt_univ_iff, lowerHemicontinuousWithinAt_iff_frequently]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousAt f x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
← upperHemicontinuousWithinAt_univ_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ UpperHemicontinuousWithinAt f univ x ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ 0 < a⁻¹

Tactic:
lift a to ℝ using ⟨h', ne_bot_of_gt h⟩
  rw [← coe_inv a]; norm_cast at *; exact inv_pos_of_pos h

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

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

Tactic:
rw [mul_comm, EReal.mul_div, mul_comm]

Goal state after:
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
⊢ ∃ a ∈ s, IsMinOn f s a

Tactic:
simp only [isMinOn_iff]
  have _ : Nonempty α := Exists.nonempty ne_s
  have _ : Nonempty s := Nonempty.to_subtype ne_s
  let φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
  let ℱ : Filter α := ⨅ a : s, φ (f a)
  have : ℱ.NeBot := by
    apply iInf_neBot_of_directed _ _
    · change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)
      exact Directed.mono_comp GE.ge (fun x y hxy ↦
        principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy)))
        (Std.Total.directed _)
    · intro x
      have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
      exact neBot_of_le this
  have hℱs : ℱ ≤ 𝓟 s :=
    iInf_le_of_le (Classical.choice inferInstance) (principal_mono.mpr <| inter_subset_left)
  have hℱ (x) (hx : x ∈ s) : ∀ᶠ y in ℱ, f y ≤ f x :=
    mem_iInf_of_mem ⟨x, hx⟩ (by apply inter_subset_right)
  obtain ⟨a, ha, h⟩ := hs hℱs
  refine ⟨a, ha, fun x hx ↦ le_of_not_gt fun hxa ↦ ?_⟩
  let _ : (𝓝 a ⊓ ℱ).NeBot := h
  suffices ∀ᶠ _ in 𝓝 a ⊓ ℱ, False by rwa [eventually_const] at this
  filter_upwards [(hf a ha (f x) hxa).filter_mono (inf_le_inf_left _ hℱs),
    (hℱ x hx).filter_mono (inf_le_right : 𝓝 a ⊓ ℱ ≤ ℱ)] using fun y h₁ h₂ ↦ not_le_of_gt h₁ h₂

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

Goal state before:
pp: α : Type u_4
⊢ ∑' (x : α), 1 = ↑(ENat.card α)

Tactic:
by
  rw [← tsum_univ]; simpa [encard_univ] using tsum_set_one univ

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

Goal state before:
pp: case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ
h1 : ↑x✝¹ ≤ x
h2 : x ∈ {⊤}ᶜ
⊢ x ∈ Ico ↑x✝¹ ⊤

Tactic:
simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

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)
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, s i) ≤ ∑' (a : ℕ), (μ (s a) + ↑(ε' a))

Tactic:
refine le_trans ?_ (ENNReal.tsum_le_tsum fun i => le_of_lt (hf i).2)

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, s i) ≤ ∑' (a : ℕ) (i : ℕ), m (f a i)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ ↑C.toReal / ↑n = ↑(C.toReal / ↑n)

Tactic:
← coe_coe_eq_natCast n,

Goal state after:
C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
n : ℕ
⊢ ↑C.toReal / ↑↑n = ↑(C.toReal / ↑n)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ x / ↑n) atTop (𝓝 (x * 0))

Tactic:
div_eq_mul_inv

Goal state after:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ x * (↑n)⁻¹) atTop (𝓝 (x * 0))
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ x * (↑n)⁻¹) atTop (𝓝 (x * 0))

Tactic:
exact tendsto_const_nhds.mul tendsto_inv_atTop_nhds_zero_nat

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
⊢ a < u x → b < v x → c < u x * v x

Tactic:
xa

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
⊢ b < v x → c < u x * v x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ n * u 0 ≤ u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h <;>
    simp [_root_.pow_succ', mul_assoc]

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

Goal state before:
pp: case e'_5
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n

Tactic:
simp only [one_div, inv_pow]

Goal state after:
case e'_5
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (2 ^ n)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case e'_5
a : ℝ
⊢ (fun n ↦ a / 2 / 2 ^ n) = fun i ↦ a / 2 * (1 / 2) ^ i

pp: case e'_6
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹

Tactic:
· funext n
    simp only [one_div, inv_pow]
    rfl

Goal state after:
case e'_6
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inl
r : ℝ≥0
hr' hr : r < 1
⊢ ∑' (n : ℕ), ↑(r ^ n) = (↑(1 - r))⁻¹

Tactic:
convert! ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)

Goal state after:
r : ℝ≥0
hr' hr : r < 1
⊢ (↑(1 - r))⁻¹ = ↑(1 - r)⁻¹
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 α
⊢ t1 ∈ ⋃ n, p n → ∀ t ∈ ⋃ n, p n, (t1 ∩ t).Nonempty → t1 ∩ t ∈ ⋃ n, p n

Tactic:
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 : Set α
ht1 : t1 ∈ ⋃ n, p n
⊢ ∀ t ∈ ⋃ n, p n, (t1 ∩ t).Nonempty → t1 ∩ t ∈ ⋃ n, p n
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f

Tactic:
suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
    rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
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
β₂ : Type u_11
inst✝¹ : MeasurableSpace β₁
inst✝ : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x✝ : Set (α₂ → β₂)
h : MeasurableSet x✝
⊢ MeasurableSet (⇑(hα.arrowCongr' ↑hβ) ⁻¹' x✝)

Tactic:
exact MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.measurable.comp (measurable_pi_apply _)

Goal state after:
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)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

Tactic:
by
        rw [← hf.2.1]
        rintro _ ⟨s, hs, rfl⟩
        simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ.toOuterMeasure (f '' t) = μ.toOuterMeasure (f '' t ∩ f '' s) + μ.toOuterMeasure (f '' t \ f '' s)

Tactic:
exact (measure_inter_add_sdiff₀ _ (hf.2 s hs)).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
s : Set β
hs : MeasurableSet s
⊢ (comap f μ) (f ⁻¹' s) = μ (s ∩ range f)

Tactic:
rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ ∑ b ∈ s, μ (f ⁻¹' {b}) = μ (f ⁻¹' ↑s)

Tactic:
by
  simp only [← measure_biUnion_finset (pairwiseDisjoint_fiber f s) hf,
    Finset.set_biUnion_preimage_singleton]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ μ (t i) ≠ ∞

Tactic:
← measure_congr (hst i)

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
i : ι
hi : μ (s i) ≠ ∞
this : Nonempty ι
t : ι → Set α := fun i ↦ s i ∩ {ω | Monotone fun x ↦ ω ∈ s x}
hst : ∀ (i : ι), s i =ᵐ[μ] t i
hMono : Monotone t
⊢ μ (s i) ≠ ∞
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:
by
  rw [← Antitone.measure_iInter]
  · rw [iInter_comm]
    exact congrArg μ <| iInter_congr fun i ↦ (biInf_const nonempty_Ici).symm
  · exact fun i j h ↦ biInter_mono (Iic_subset_Iic.2 h) fun _ _ ↦ Set.Subset.rfl
  · exact fun i ↦ .biInter (to_countable _) fun _ _ ↦ h _
  · refine hfin.imp fun k hk ↦ ne_top_of_le_ne_top hk <| measure_mono <| iInter₂_subset k ?_
    rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t : Set α
ht : t ∈ measurableAtom '' s
t' : Set α
⊢ t' ∈ measurableAtom '' s → t ≠ t' → Disjoint t t'

Tactic:
ht'

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t : Set α
ht : t ∈ measurableAtom '' s
t' : Set α
ht' : t' ∈ measurableAtom '' s
⊢ t ≠ t' → Disjoint t t'
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen[inst✝²] K})

Tactic:
refine
    ⟨{  set := f
        set_mem := fun n => (fS n).1
        finite := fun n => (fS n).2
        spanning := ?_ }⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
T_ne : T.Nonempty
f : ℕ → Set α
hf : T = range f
fS : ∀ (n : ℕ), f n ∈ S
⊢ ⋃ i, f i = univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ae (μ.restrict (s ∪ t)) = ae (μ.restrict s) ⊔ ae (μ.restrict t)

Tactic:
by
  simp [union_eq_iUnion, iSup_bool_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : SeparatesPoints α
⊢ CountablySeparated α

Tactic:
rcases h with ⟨b, hbc, hb⟩
  refine ⟨⟨b, hbc, fun t ht ↦ hb.symm ▸ .basic t ht, ?_⟩⟩
  rw [hb] at ‹SeparatesPoints _›
  convert! separating_of_generateFrom b
  simp

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

Goal state before:
pp: case refine_1.hC
α : Type u_1
t : ℕ → Set α
n : ℕ
s u : Set α
hu : u ∈ memPartition t n
ht✝ : MeasurableSet u
⊢ ∃ S, ↑S ⊆ memPartition t n ∧ u = ⋃₀ ↑S

Tactic:
| hC u hu _ =>

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

Goal state before:
pp: α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ ν : Measure α
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f ν
s : Set δ
hs : MeasurableSet s
⊢ (map f μ) s ≤ (map f ν) s

Tactic:
by simpa [hf, hs, hf.mono_measure h] using h (f ⁻¹' s)

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
⊢ ∑ i, f i = f true + f false

Tactic:
Fintype.sum_bool

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
⊢ f true + f false = f true + f false
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: case neg
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst✝³] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst✝³] s
h1 : s.Nonempty
h2 : ¬s = univ
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
exact hf s hs h1 h2

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

Goal state before:
pp: case mpr
α : 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 α) := ⋯
this : MeasurableSpace α := ⋯
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 : α
⊢ (∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 ∈ t) (_ : i < i_1) (_ : i_1 ≤ a), i ≤ y ∧ y < i_1) → y < a

Tactic:
· rintro ⟨l, -, u, -, -, hua, -, hyu⟩
        exact hyu.trans_le hua

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ hausdorffEDist s t ≤ ENNReal.ofReal (max rs rt)

Tactic:
apply hausdorffEDist_le_of_mem_edist

Goal state after:
case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)

case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case e'_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ mα = MeasurableSpace.generateFrom ?convert_2

pp: case convert_2
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ Set (Set α)

pp: case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ ∀ t ∈ ?convert_2, MeasurableSet (f ⁻¹' t)

Tactic:
· exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Iio _)

Goal state after:
case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)
⊢ ∀ t ∈ range Iio, MeasurableSet (f ⁻¹' t)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
⊢ map g (f.restrict s) = (map g f).restrict s

Tactic:
by
  classical
  exact ext fun x =>
    if hs : MeasurableSet s then by simp [hs, Set.indicator_comp_of_zero hg]
    else by simp [restrict_of_not_measurable hs, hg]

Goal state after: