mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖y‖

Tactic:
exact hr ‹_›

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
a b c : IterateMulAct f
⊢ a * b * c = a * (b * c)

Tactic:
ext; apply Nat.add_assoc

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂₀ s)

Tactic:
sInter_eq_biInter

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂ i ∈ s, i)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
⊢ NoncompactSpace E

Tactic:
· rcases exists_ne (0 : E) with ⟨x, hx⟩
    suffices IsClosedEmbedding (Infinite.natEmbedding 𝕜 · • x) from this.noncompactSpace
    refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_
    simp only [dist_eq_norm, ← sub_smul, norm_smul]
    rw [H, one_mul]
    rwa [sub_ne_zero, (Embedding.injective _).ne_iff]

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

Goal state before:
pp: α : Type u_1
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
ι : Sort u_4
f : ι → OuterMeasure α
c : R
s : Set α
⊢ (c • ⨆ i, f i) s = (⨆ i, c • f i) s

Tactic:
simp only [smul_apply, iSup_apply, ENNReal.smul_iSup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (i : ℕ) (i_1 : ι), (f i_1) (s i)

Tactic:
rw [ENNReal.tsum_comm]; exact ENNReal.tsum_le_tsum fun i => measure_iUnion_le _

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
⊢ Measurable fun x ↦ if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i

Tactic:
by_cases h : i ∈ s <;> simp [h, Measurable.eval, measurable_fst, measurable_snd]

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

Goal state before:
pp: f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
not_summable_iff_tendsto_nat_atTop_of_nonneg hf

Goal state after:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop ↔ Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : sign a = -1
⊢ a < 0

Tactic:
sign_apply

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed[inst✝³] ↑s
hx : x ∈ s
⊢ {x} ⊆ ↑s

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.Data.Sign.Defs

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

Tactic:
sign_apply

Goal state after:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0
Module: Mathlib.Data.Sign.Defs

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

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

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

Tactic:
· simp [h, h.le]

Goal state after:
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: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
· simp [h, h.le]

Goal state after:
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:
← EReal.coe_mul,

Goal state after:
case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ↑(a * ↑n) ≤ ↑↑m
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
⊢ c / b = a ↔ c = a * b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
  · rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

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

Goal state before:
pp: case pos
x : EReal
h_top : x = ⊤
n : ℕ
⊢ ∀ᶠ (a : EReal) in 𝓝 ⊤, ↑n < a.toENNReal

Tactic:
filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy

Goal state after:
x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : ↑↑n < y
⊢ ↑n < y.toENNReal
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
exact c_ab.trans (add_lt_add a_x b_x)

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

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

pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
· rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
    norm_cast at *
    convert! ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
    rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]

Goal state after:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
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 < p.1

Tactic:
apply lt_of_le_of_lt _ p1_gt

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.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
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < ↑(2 * max (x + 1) 0 / a) * ↑(a / 2)

Tactic:
← EReal.coe_mul,

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
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < ↑(2 * max (x + 1) 0 / a * (a / 2))
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
Set.mem_iUnion

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 : ∃ i, t1 ∈ p i
t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
⊢ ∃ i, t1 ∩ t2 ∈ p i
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: p : EReal × EReal
h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥
h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤
h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0
h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) p

Tactic:
by
  rcases p with ⟨x, y⟩
  induction x <;> induction y
  · exact continuousAt_mul_symm3 continuousAt_mul_top_top
  · simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃
    exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)
  · exact EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top
  · simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁
    exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))
  · exact continuousAt_mul_coe_coe _ _
  · simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂
    exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)
  · exact continuousAt_mul_symm2 continuousAt_mul_top_top
  · simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄
    exact continuousAt_mul_top_ne_zero h₄
  · exact continuousAt_mul_top_top

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

Goal state before:
pp: case mp
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

pp: case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤
          (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
· intro h t _ht
    exact h t

Goal state after:
case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤
          (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ s', MeasurableSet s' ∧ (fun x ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
MeasurableSpace.measurableSet_top,

Goal state after:
α : Type u_1
s t : Set α
⊢ (∃ s', True ∧ (fun x ↦ x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case mp
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

pp: case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t

Tactic:
· rintro ⟨x, rfl⟩
    by_cases hT : True ∈ x
    · by_cases hF : False ∈ x
      · suffices x = univ by grind
        grind [univ_eq_true_false]
      · grind
    · by_cases hF : False ∈ x
      · grind
      · suffices x ⊆ ∅ by grind
        intro p hp
        fin_cases p <;> contradiction

Goal state after:
case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t
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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
⊢ α ≃ᵐ β

Tactic:
suffices Σ' A : Set α, MeasurableSet A ∧ F A = A by
    classical
    rcases this with ⟨A, Ameas, Afp⟩
    let B := f '' A
    have Bmeas : MeasurableSet B := hf.measurableSet_image' Ameas
    refine (MeasurableEquiv.sumCompl Ameas).symm.trans
      (MeasurableEquiv.trans ?_ (MeasurableEquiv.sumCompl Bmeas))
    apply MeasurableEquiv.sumCongr (hf.equivImage _)
    have : Aᶜ = g '' Bᶜ := by
      apply compl_injective
      rw [← Afp]
      simp [F, B]
    rw [this]
    exact (hg.equivImage _).symm

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 γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
⊢ (A : Set α) ×' MeasurableSet A ∧ F A = A
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = x

Tactic:
nth_rw 3 [← hf.equivRange.symm_apply_apply x]
  rw [hf.equivRange_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : α → β
hs : s.Countable
⊢ μ (⋃ y ∈ s, f ⁻¹' {y}) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0

Tactic:
measure_biUnion_null_iff hs

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : α → β
hs : s.Countable
⊢ (∀ i ∈ s, μ (f ⁻¹' {i}) = 0) ↔ ∀ x ∈ s, μ (f ⁻¹' {x}) = 0
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:

Tactic:
a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

Tactic:
rw [restrict_apply' hs]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : s ⊆ t
h : μ.restrict t = ν.restrict t
⊢ μ.restrict s = ν.restrict s

Tactic:
by
  rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ae (μ.restrict s) = ae μ ⊓ 𝓟 s

Tactic:
ext t
  simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_ofPred,
    Classical.not_imp, fun a => and_comm (a := a ∈ s) (b := a ∉ t)]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
⊢ MeasurableSingletonClass α

Tactic:
rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
⊢ MeasurableSingletonClass α
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.compl.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ (⋃₀ ↑S)ᶜ = ⋃₀ ↑((memPartition t n).toFinset \ S)

Tactic:
simp only [Finset.coe_sdiff, coe_toFinset]
        refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm
        · refine Set.disjoint_sUnion_right.mpr fun u huS => ?_
          refine Set.disjoint_sUnion_left.mpr fun v huV => ?_
          refine disjoint_memPartition t n (mem_of_mem_sdiff huV) (hS_subset huS) ?_
          exact ne_of_mem_of_not_mem huS (notMem_of_mem_sdiff huV) |>.symm
        · rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_sdiff_cancel hS_subset]

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

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

Tactic:
exact ⟨Or.inr h⟩

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

Goal state before:
pp: case refine_3
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
⊢ f =ᵐ[μ] g

Tactic:
have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
    filter_upwards [compl_mem_ae_iff.2 A] with x hx
    rw [mem_compl_iff] at hx
    simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
    contrapose! hx
    apply subset_toMeasurable
    simp only [hx, mem_compl_iff, mem_ofPred_eq, false_and, not_false_iff]

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
h : NullMeasurable f μ
inst✝ : MeasurableSpace.CountablyGenerated ↑∅
hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅
⊢ AEMeasurable f μ

Tactic:
obtain rfl : μ = 0 := by simpa using hft
    apply aemeasurable_zero_measure

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u

Tactic:
exact GenerateOpen.basic _ hu

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α✝
α : Type u_6
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
h : OpensMeasurableSpace α
p : α → Prop
⊢ MeasurableSpace.comap val (borel α) ≤ instMeasurableSpace

Tactic:
exact comap_mono h.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
a : α
⊢ (⨅ s ∈ {s | a ∈ s ∧ IsOpen[inst✝¹²] s}, 𝓟 s).IsMeasurablyGenerated

Tactic:
iInf_subtype'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
a : α
⊢ (⨅ x, 𝓟 ↑x).IsMeasurablyGenerated
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

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

Tactic:
by
  constructor
  have : Pi.topologicalSpace = .generateFrom { t | ∃ (s : ∀ a, Set (X a)) (i : Finset ι),
      (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = pi (↑i) s } := by
    simp +instances only [funext fun a => @eq_generateFrom_countableBasis (X a) _ _,
      pi_generateFrom_eq]
  rw [borel_eq_generateFrom_of_subbasis this]
  apply generateFrom_le
  rintro _ ⟨s, i, hi, rfl⟩
  refine MeasurableSet.pi i.countable_toSet fun a ha => IsOpen.measurableSet ?_
  rw [eq_generateFrom_countableBasis (X a)]
  exact .basic _ (hi a ha)

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

Goal state before:
pp: case pos
α : 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 = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc 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
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ MeasurableSet (⋃ (_ : a < b), ⋃ (_ : b < a✝), Icc a b)

Tactic:
refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_

Goal state after:
case pos
α : 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 = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc 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
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a < b
x✝ : b < a✝
⊢ MeasurableSet (Icc a b)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ x ∉ Uᶜ

Tactic:
simpa using hx

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ hausdorffEDist s t

Tactic:
hausdorffEDist_def

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s)