mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
| cons a s ha hne ihs =>

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

Goal state before:
pp: M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsIsometricSMul M X
c : ULift.{u_2, u} M
⊢ Isometry fun x ↦ c • x

Tactic:
by simpa only using! isometry_smul X c.down

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)

Tactic:
dist_eq_norm',

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ / (‖z‖ * ‖w‖)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (𝓝[≠] 0)⁻¹ = cobounded α

Tactic:
← inv_cobounded₀,

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (cobounded α)⁻¹⁻¹ = cobounded α
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) ↔ MeasurableSet s

Tactic:
by
  constructor <;> intro h
  · convert! h (MeasurableSet.singleton (0 : β)).compl
    ext a
    simp [NeZero.ne b]
  · exact measurable_const.indicator h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
ms : Set (OuterMeasure α)
f : ℕ → Set α
x✝ : Pairwise (Disjoint on f)
m : OuterMeasure α
hm : m ∈ ms
i : ℕ
⊢ m (f i) ≤ ⨆ m ∈ ms, m (f i)

Tactic:
apply le_iSup₂ m hm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
ms : Set (OuterMeasure α)
m : OuterMeasure α
hm : m ∈ ms
s : Set α
⊢ m s ≤ (sSup ms) s

Tactic:
apply le_iSup₂ m hm

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

Goal state before:
pp: case inl
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : s.pi t = ∅
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

pp: case inr
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅

Tactic:
· simp [h]

Goal state after:
case inr
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi t = ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x ↦ (Equiv.piEquivPiSubtypeProd p X).symm x j

Tactic:
by_cases hj : p j

Goal state after:
case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x ↦ (Equiv.piEquivPiSubtypeProd p X).symm x j

case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x ↦ (Equiv.piEquivPiSubtypeProd p X).symm x j
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ 0 < ∑ i ∈ s, f i

Tactic:
exact Finset.sum_pos h hs

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
rcases trichotomy (sign b) with hsb | hsb | hsb

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
rcases trichotomy (sign b) with hsb | hsb | hsb

Goal state after:
case inr.inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
rcases trichotomy (sign b) with hsb | hsb | hsb

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
g : β → ℝ≥0∞
⊢ ∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))

Tactic:
simp only [surjInv_eq hf]

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

Tactic:
← lowerHemicontinuousWithinAt_univ_iff,

Goal state after:
α : 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
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ BddBelow (f '' s)

Tactic:
by
  cases s.eq_empty_or_nonempty with
  | inl h =>
      simp only [h, Set.image_empty]
      exact bddBelow_empty
  | inr h =>
      obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_isMinOn h hs hf
      exact has.bddBelow

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
hd : tsum d ≠ ∞
⊢ CauchySeq f

Tactic:
by
  lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i
  rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd
  exact cauchySeq_of_edist_le_of_summable d hf hd

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
· rw [h, bot_add]

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

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

Tactic:
h₁

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
a✝ : α × γ
h₁ : a✝.1 ∈ sᶜ
⊢ a✝.1 ∈ s → a✝.2 < f a✝.1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ limsup u f * c ≤ limsup (fun x ↦ u x * c) f

Tactic:
· rw [le_limsup_iff]
    simpa [← EReal.div_lt_iff (by aesop) (by aesop)]
      using fun _ ↦ frequently_lt_of_lt_limsup

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

Goal state before:
pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
· simp [h]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty
⊢ f ⁻¹' s ∩ f ⁻¹' t ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
← Set.preimage_inter

Goal state after:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ f ⁻¹' (s ∩ t) ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case e'_4
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t

pp: case inr.convert_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ m (t ∩ s) + m (t \ s)

Tactic:
· simp [h]

Goal state after:
case inr.convert_2
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
t : Set α
h : t.Nonempty
⊢ (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ m (t ∩ s) + m (t \ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * m t = a * m (t ∩ s) + a * m (t \ s)

Tactic:
(isCaratheodory_iff m).mp h t

Goal state after:
α : Type u_1
a : ℝ≥0∞
m : OuterMeasure α
s : Set α
h : MeasurableSet s
t : Set α
⊢ a * (m (t ∩ s) + m (t \ s)) = a * m (t ∩ s) + a * m (t \ s)
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
rw [Finset.mem_singleton] at hx

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

Goal state before:
pp: α : 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
⊢ ⨅ (ht : P (⇑f ⁻¹' s)), ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ht = ⨅ (ht : P s), ⨅ (_ : A ⊆ s), m s ht

Tactic:
refine iInf_congr_Prop (Pm s) ?_

Goal state after:
α : 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₂
f : α ≃ α
Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s
mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs
A s : Set α
⊢ ∀ (x : P s), ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s x
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (s : Set α), μ sᶜ = 0 ↔ s = univ
a : α
ha : μ {a} = 0
⊢ False

Tactic:
by simpa [ha] using (h {a}ᶜ).1

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

Goal state before:
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 α
h :
  ∀ (t : Set α),
    P t →
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
u : Set α
⊢ (inducedOuterMeasure m P0 m0) (u ∩ s) + (inducedOuterMeasure m P0 m0) (u \ s) ≤ (inducedOuterMeasure m P0 m0) u

Tactic:
conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]

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 α
h :
  ∀ (t : Set α),
    P t →
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
u : Set α
⊢ (inducedOuterMeasure m P0 m0) (u ∩ s) + (inducedOuterMeasure m P0 m0) (u \ s) ≤
    ⨅ t, ⨅ (ht : P t), ⨅ (_ : u ⊆ t), m t ht
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
t : Set α
ht : t ∈ {s}
⊢ (fun x ↦ x ∈ s) ⁻¹' {True} = t

Tactic:
simp [ht.symm]

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

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

Tactic:
hp

Goal state after:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
⊢ p ∈ ∅
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

Tactic:
rw [this, measure_iUnion]

Goal state after:
case hn
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ Pairwise (Disjoint on fun x ↦ {(x, y)})

case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ ∀ (i : α), MeasurableSet {(i, y)}
Module: Mathlib.MeasureTheory.Measure.Comap

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

Tactic:
by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β)

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0
⊢ comap f 0 = 0

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : ¬(Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) 0)
⊢ comap f 0 = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᵐ[μ] s ↔ t ≤ᵐ[μ] s

Tactic:
by
  rw [ae_le_set]
  refine
    ⟨fun h => by simpa only [union_sdiff_left] using (ae_eq_set.mp h).1, fun h =>
      eventuallyLE_antisymm_iff.mpr
        ⟨by rwa [ae_le_set, union_sdiff_left],
          LE.le.eventuallyLE subset_union_left⟩⟩

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✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ SFinite (μ + ν)

Tactic:
have : ∀ b : Bool, SFinite (cond b μ ν) := by simp [*]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
this : ∀ (b : Bool), SFinite (bif b then μ else ν)
⊢ SFinite (μ + ν)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
⊢ (c • μ).FiniteAtFilter (𝓝 x)

Tactic:
rcases μ.exists_isOpen_measure_lt_top x with ⟨o, xo, o_open, μo⟩

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ✝ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
c : ℝ≥0
x : α
o : Set α
xo : x ∈ o
o_open : IsOpen[inst✝¹] o
μo : μ o < ∞
⊢ (c • μ).FiniteAtFilter (𝓝 x)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ (i : ι), NullMeasurableSet (s i) μ
hm : Antitone s
hf : ∃ i, μ (s i) ≠ ∞
h : atTop.NeBot
this : IsDirectedOrder ι
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨅ i, μ (s i)))

Tactic:
exact tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm

Goal state after:
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 ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D

Tactic:
have A n : ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] (⋃₀ D) :=
    exists_ae_subset_biUnion_countable_of_isFiniteMeasure hC

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
A : ∀ (n : ℕ), ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] ⋃₀ D
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ x, s ↑x)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
ae_restrict_iUnion_eq,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ⨆ i, ae (μ.restrict (s ↑i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ (∀ᵐ (x : α) ∂μ.restrict (⋃ i, s i), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x

Tactic:
ae_restrict_iUnion_eq,

Goal state after:
α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
f g : α → δ
⊢ (∀ᶠ (x : α) in ⨆ i, ae (μ.restrict (s i)), f x = g x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), f x = g x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ inst✝¹ = generateFrom (⋃ y, {measurableAtom y})

Tactic:
refine le_antisymm ?_ (generateFrom_le (by simp [MeasurableSet.measurableAtom_of_countable]))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ inst✝¹ ≤ generateFrom (⋃ y, {measurableAtom y})
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ f =ᵐ[μ.restrict s] g ↔ s.indicator f =ᵐ[μ] s.indicator g

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
⊢ (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) ↔ s.indicator f =ᵐ[μ] s.indicator g
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed[inst✝¹] t
T_open : ∀ t ∈ ∅, IsOpen[inst✝¹] t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover ∅ t

Tactic:
exact t.hasSeparatingCover_empty_left

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: case ofNat
α✝ : Type u_1
M✝ : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : SMul M✝ X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M✝
g : α → X
inst✝⁵ : MeasurableSpace M✝
inst✝⁴ : MeasurableSMul M✝ X
M : Type u_6
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℕ
⊢ Measurable fun x ↦ (x, Int.ofNat n).2 • (x, Int.ofNat n).1

Tactic:
simp only [Int.ofNat_eq_natCast, natCast_zsmul]
      exact measurable_const_smul _

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ

Tactic:
induction l with
  | nil => exact aemeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEDist x t ≤ r
H2 : ∀ x ∈ t, infEDist x s ≤ r
⊢ hausdorffEDist s t ≤ r

Tactic:
by
  simp only [hausdorffEDist_def, sup_le_iff, iSup_le_iff]
  exact ⟨H1, H2⟩

Goal state after: