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

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(-(-a)⁻¹) = ↑a⁻¹

Tactic:
← _root_.inv_neg,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(- -a)⁻¹ = ↑a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ ↑a⁻¹

Tactic:
EReal.coe_nonneg,

Goal state after:
case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
b_0 : 0 < b
a : ℝ
a_b : ↑a < b
a_0 : 0 < ↑a
⊢ b⁻¹ < (↑a)⁻¹

Tactic:
match b with
  | ⊤ => exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)
  | ⊥ => exact (not_lt_bot b_0).rec
  | (b : ℝ) =>
    rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]
    exact _root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0)
      (EReal.coe_lt_coe_iff.1 a_b)

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

Goal state before:
pp: m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
exact Nat.cast_div_le

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

Goal state before:
pp: ⊢ (range ENNReal.toEReal).OrdConnected

Tactic:
rw [range_coe_ennreal]; exact ordConnected_Ici

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

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

Tactic:
rw [limsup_le_iff]
    simpa [← EReal.lt_div_iff (by aesop) (by aesop)]
      using fun _ ↦ eventually_lt_of_limsup_lt

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : ExistsAddOfLE α
inst✝ : Archimedean α
r : α
h : 1 < r
⊢ Tendsto (fun n ↦ r ^ n) atTop atTop

Tactic:
obtain ⟨r, r0, rfl⟩ := exists_pos_add_of_lt' h

Goal state after:
α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : ExistsAddOfLE α
inst✝ : Archimedean α
r : α
r0 : 0 < r
h : 1 < 1 + r
⊢ Tendsto (fun n ↦ (1 + r) ^ n) atTop atTop
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = ∑ i ∈ Finset.range n, 1

Tactic:
sum_const,

Goal state after:
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = #(Finset.range n) • 1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ ∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1

Tactic:
by
  simp_rw [neg_sub_left, ENNReal.zpow_neg, ← Nat.cast_one (R := ℤ), ← Nat.cast_add, zpow_natCast,
    ENNReal.inv_pow, ENNReal.tsum_geometric_add_one, one_sub_inv_two, inv_inv]
  exact ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' 2)) (Ne.symm top_ne_ofNat)

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

Goal state before:
pp: a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (-a, b)

Tactic:
have : (fun p : EReal × EReal ↦ p.1 * p.2) = (fun x : EReal ↦ -x)
      ∘ (fun p : EReal × EReal ↦ p.1 * p.2) ∘ (fun p : EReal × EReal ↦ (-p.1, p.2)) := by
    ext p
    simp
  rw [this]
  apply ContinuousAt.comp (Continuous.continuousAt continuous_neg)
    <| ContinuousAt.comp _ (ContinuousAt.prodMap (Continuous.continuousAt continuous_neg)
      (Continuous.continuousAt continuous_id))
  simp [h]

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

Goal state before:
pp: case h.refine_1
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 * 1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
rw [mul_one p.1] at this

Goal state after:
case h.refine_1
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s

Tactic:
by
  rw [le_boundedBy, forall_congr']
  intro s
  rcases s.eq_empty_or_nonempty with h | h <;> simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
refine le_sInf ?_

Goal state after:
case refine_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ ∀ b ∈ m, boundedBy (sInfGen m) ≤ b
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ LowerSemicontinuousOn f⁻¹ s ↔ UpperSemicontinuousOn f s

Tactic:
by
  simp [lowerSemicontinuousOn_iff, upperSemicontinuousOn_iff]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t : Set α
ht : t ∈ generatePiSystem S
⊢ t ∈ generatePiSystem T

Tactic:
induction ht with

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

Goal state before:
pp: case intro.m0
α : 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)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
hm : ∀ (i : β), P (f i)
val✝ : Encodable β
⊢ extend m ∅ = 0

Tactic:
exact extend_empty P0 m0

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x}

Tactic:
· rcases h with hs | hs
    · refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
      · rw [Finset.coe_singleton]
      · rw [Finset.mem_singleton] at hx
        rwa [hx]
      · simp only [Finset.mem_singleton, iInter_iInter_eq_left]
    · refine ⟨∅, ?_⟩
      simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
        imp_true_iff, Finset.notMem_empty, iInter_false, iInter_univ, true_and,
        exists_const] using! hs

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, f i)

Tactic:
← Encodable.iUnion_decode₂

Goal state after:
case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ C t ⋯

Tactic:
induction ht with

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

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

Tactic:
by
  rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]

Goal state after:
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 ((rangeSplitting g ∘ rangeFactorization g) ∘ f)

Tactic:
exact hg.measurable_rangeSplitting.comp H.subtype_mk

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
⊢ Pairwise (Disjoint on fun i ↦ s i \ (fun i ↦ toMeasurable μ (s i ∩ ⋃ j ∈ {i}ᶜ, s j)) i)

Tactic:
simp only [Pairwise, disjoint_left, onFun, mem_sdiff, not_and, and_imp, Classical.not_not]
    intro i j hne x hi hU hj
    replace hU : x ∉ s i ∩ iUnion fun j ↦ iUnion fun _ ↦ s j :=
      fun h ↦ hU (subset_toMeasurable _ _ h)
    simp only [mem_inter_iff, mem_iUnion, not_and, not_exists] at hU
    exact (hU hi j hne.symm hj).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ) s = μ (f ⁻¹' s)

Tactic:
liftLinear_apply₀ _ hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((OuterMeasure.map (AEMeasurable.mk f hf)) μ.toOuterMeasure) s = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
map_of_not_aemeasurable hfm

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : 0 = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ 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
⊢ g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)

Tactic:
smul_set_inter,

Goal state after:
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
⊢ g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)

Tactic:
← Finset.sum_attach,

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ μ (⋃ b ∈ s, f b) = ∑ x ∈ s.attach, μ (f ↑x)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : μ s ≠ ∞
⊢ μ sᶜ = μ univ - μ s

Tactic:
rw [← measure_add_measure_compl₀ h, ENNReal.add_sub_cancel_left hs]

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) μ
hfin : ∃ i, μ (s i) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
obtain ⟨i, hi⟩ := hfin

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) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞) → ∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
rintro s t hst ⟨U, htU, hUo, hU⟩

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ x ∈ s✝, μ.FiniteAtFilter (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen[inst✝¹] U
hU : μ U < ∞
⊢ ∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : 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
x : α
⊢ ∃ t ∈ range f, x ∈ t

Tactic:
by
    have : x ∈ ⋃₀ T := by simp only [hT, mem_univ]
    simpa only [mem_sUnion, exists_prop, ← hf]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
hc : c ≠ 0
μ : Measure α
⊢ ae (c • μ) = ae μ

Tactic:
by ext; exact ae_ennreal_smul_measure_iff hc

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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t = μ (toMeasurable (μ + ν) t)

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t ≠ ∞

Tactic:
· refine
      measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm
    rwa [measure_toMeasurable t]

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ∞
⊢ μ t ≠ ∞
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
⊢ HasCountableSeparatingOn α p t

Tactic:
refine ⟨⟨V '' S, hSc.image _, forall_mem_image.2 hpV, fun x hx y hy h ↦ ?_⟩⟩

Goal state after:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h✝ : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
x : α
hx : x ∈ t
y : α
hy : y ∈ t
h : ∀ s ∈ V '' S, x ∈ s ↔ y ∈ s
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: β : Type u_2
m₂ : MeasurableSpace β
h₂ : CountablyGenerated β
b₁ : Set (Set β)
hb₁c : b₁.Countable
⊢ CountablyGenerated β

Tactic:
rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩

Goal state after:
β : Type u_2
b₁ : Set (Set β)
hb₁c : b₁.Countable
b₂ : Set (Set β)
hb₂c : b₂.Countable
⊢ CountablyGenerated β
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
⊢ ∃ q, ∅ = ⋃ p, if q p then countablyGeneratedAtom α p else ∅

Tactic:
exact ⟨fun _ ↦ False, by simp⟩

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

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0 x
x : α
hx : x ∈ s → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = 0 x

Tactic:
· simp [hxs]

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

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
A : ℕ → Set α := natGeneratingSequence α
hA : ∀ (n : ℕ), MeasurableSet (A n)
hA_gen : generateFrom (range A) = mα
⊢ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ A x_1

Tactic:
exact mem_countablyGeneratedAtom_natGeneratingSequence x

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

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
x : α
hx : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.indicator f x = s.indicator g x

Tactic:
· simp [hxs]

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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
m : ℝ≥0∞
x✝ : m ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t : Set α
ht₁ : m = μ (t ∩ s) + ν (tᶜ ∩ s)
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t n) ≤ m

Tactic:
subst ht₁
    -- We first show `(μ ⊓ ν) s ≤ μ (t ∩ s) + ν (tᶜ ∩ s)` for any `t : Set α`
    -- For this, define the sequence `t' : ℕ → Set α` where `t' 0 = t ∩ s`, `t' 1 = tᶜ ∩ s` and
    -- `∅` otherwise. Then, we have by construction
    -- `(μ ⊓ ν) s ≤ ∑' n, μ (t' n) ⊓ ν (t' n) ≤ μ (t' 0) + ν (t' 1) = μ (t ∩ s) + ν (tᶜ ∩ s)`.
    set t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅ with ht'
    refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_
    · by_cases hxt : x ∈ t
      · refine mem_iUnion.2 ⟨0, ?_⟩
        simp [hx, hxt]
      · refine mem_iUnion.2 ⟨1, ?_⟩
        simp [hx, hxt]
    · simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
      rw [tsum_eq_add_tsum_ite 0, tsum_eq_add_tsum_ite 1, if_neg zero_ne_one.symm,
        ENNReal.summable.tsum_eq_zero_iff.2 _, add_zero]
      · exact add_le_add (inf_le_left.trans <| by simp [ht']) (inf_le_right.trans <| by simp [ht'])
      · simp only [ite_eq_left_iff]
        intro n hn₁ hn₀
        simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, le_refl, inf_of_le_left]

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

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

Tactic:
obtain ⟨S, hS_subset, rfl⟩ := hu

Goal state after:
case refine_1.compl
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ∃ S_1, ↑S_1 ⊆ memPartition t n ∧ (⋃₀ ↑S)ᶜ = ⋃₀ ↑S_1
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
x : α
hx : ∃ i, ∃ (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i
⊢ x ∈ ⋃ i, s i

Tactic:
have ⟨C, ⟨_, C_nonempty⟩, hxC⟩ := hx

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
x : α
hx : ∃ i, ∃ (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i
C : Finset ι
left✝ : C ∈ F.powerset
C_nonempty : C ∉ {∅}
hxC : x ∈ P C
⊢ x ∈ ⋃ i, s i
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case pos
α : 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)
x : α
hx : x ∈ s
⊢ g x ∈ t

Tactic:
simpa [g, hx] using h₀.some_mem

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ M • (μ.restrict (⋃ C ∈ Cs, P C)) t ≤ (M • μ.restrict (⋃ i, s i)) t

Tactic:
Measure.smul_apply

Goal state after:
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
⊢ M • (μ.restrict (⋃ C ∈ Cs, P C)) t ≤ M • (μ.restrict (⋃ i, s i)) t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K s : Set γ
hK : IsCompact K
hs : MeasurableSet s
hKs : K ⊆ s
⊢ closure[inst✝³] K ⊆ s

Tactic:
by
  rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
  exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ (⨅ y ∈ s, edist x y) + ediam s

Tactic:
ENNReal.iInf_add

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
⊢ edist x y ≤ ⨅ i ∈ s, edist x i + ediam s
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
r : ℝ
hr : 0 ≤ r
hs : s.Nonempty
H1 : ∀ x ∈ s, infDist x ∅ ≤ r
H2 : ∀ x ∈ ∅, infDist x s ≤ r
⊢ hausdorffDist s ∅ ≤ r

Tactic:
hausdorffDist_empty

Goal state after:
case inr.inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
r : ℝ
hr : 0 ≤ r
hs : s.Nonempty
H1 : ∀ x ∈ s, infDist x ∅ ≤ r
H2 : ∀ x ∈ ∅, infDist x s ≤ r
⊢ 0 ≤ r