mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend f)
⊢ Continuous[instTopologicalSpaceProd, _] fun b ↦ edist (hs.extend f b.1) (hs.extend f b.2)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend f)
⊢ Continuous[instTopologicalSpaceProd, _] fun b ↦ edist b.1 b.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Submodule

Goal state before:
pp: R : Type u_3
R' : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R'
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R' M'
σ₁₂ : R →+* R'
f : M →ₛₗ[σ₁₂] M'
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
hf : Continuous ⇑f
p : Submodule R M
⊢ Continuous ((↑p).domRestrict ⇑f)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
⊢ Tendsto (fun x ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
rw [NormedGroup.tendsto_nhds_one] at hf ⊢

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
⊢ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rcases hne with ⟨x, y, hα⟩
  have hgf := (edist_eq (g.comp f) x y).symm
  simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_left_inj hα.1 hα.2]
    at hgf
  rwa [← ENNReal.coe_inj, ENNReal.coe_mul]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
rcases z.natAbs_eq with hz | hz
  · rw [← Int.cast_natCast, ← hz]
  · rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)

Tactic:
simpa [piecewise_preimage] using hs.ite (hf ht) (hg ht)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
ε : ℝ
h : 0 < ε
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun y ↦ ‖c • (y - x)‖

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n < ∞ ↔ n < ⊤

Tactic:
by simp [← toENNReal_lt]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0

Tactic:
← sUnion_range,

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ μ (⋃₀ range s) = 0 ↔ ∀ (i : ι), μ (s i) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
s : Set β
hx : x ∈ sᶜ
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
⊢ False

Tactic:
exact hx hxs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s t : Set α
h : s ⊆ t
⊢ c • m s ≤ c • m t

Tactic:
rw [← smul_one_mul c, ← smul_one_mul c (m t)]
        exact mul_right_mono (m.mono h)

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

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (i : δ) → MeasurableSpace (X i)
l : List δ
⊢ Measurable (TProd.mk l)

Tactic:
by
  induction l with
  | nil => exact measurable_const
  | cons i l ih => exact (measurable_pi_apply i).prodMk ih

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

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v ↦ v.elim hj

Tactic:
simpa using measurable_fst

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : MeasurableSet {a | p a}
⊢ MeasurableSet (p ⁻¹' {True})

Tactic:
simpa only [preimage_singleton_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable α
s t : β → Set α
hs✝ : Measurable s
hs : Measurable t
i : α
⊢ Measurable fun a ↦ i ∈ s a

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable α
s t : β → Set α
hs✝ : Measurable s
hs : Measurable t
i : α
⊢ Measurable fun a ↦ i ∈ t a

Tactic:
fun_prop

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

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
inst✝ : MeasurableSpace X
⊢ Measurable uncurry

Tactic:
fun_prop

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

Goal state before:
pp: ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst✝ : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
x✝ : Sigma κ
⊢ Measurable fun c ↦ c x✝.fst x✝.snd

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] fun r ↦ r • 1

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun n ↦ ↑(f n).toNNReal
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
h_f_coe,

Goal state after:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun n ↦ ↑(f n).toNNReal
⊢ Tendsto (fun n ↦ ↑(f n).toNNReal) cofinite (𝓝 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
constructor
  · intro h
    refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_
    exacts [Finset.sum_mono_set _, tendsto_finset_range]
  · rintro hnat ⟨r, hr⟩
    exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

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:
rw [← upperHemicontinuousWithinAt_univ_iff, upperHemicontinuousWithinAt_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).Nonempty) → (f x ∩ t).Nonempty) ↔
    ∀ (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 : a < 0
h' : a ≠ ⊥
⊢ a⁻¹ < 0

Tactic:
lift a to ℝ using ⟨ne_top_of_lt h, h'⟩

Goal state after:
a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ (↑a)⁻¹ < 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha

Goal state after:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0 * ⊤
⊢ ∃ a' ∈ Ioo 0 0, c < a' * ⊤

case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤
Module: Mathlib.Topology.Semicontinuity.Basic

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

Tactic:
| inr h =>

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

Goal state before:
pp: case h'
⊢ ∀ (i' : ℝ), True → ∃ i < ⊤, Ici i ∩ {⊤}ᶜ ⊆ Real.toEReal '' Ici i'

Tactic:
· simp only [EReal.image_coe_Ici, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

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

Goal state before:
pp: a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
⊢ c ≤ d

Tactic:
obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd

Goal state after:
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝¹ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd✝ : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
b' : EReal
bb' : b' ∈ Ioo b ⊤
hd : a' * b' < d
⊢ c ≤ d
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case a
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ∀ (i : ℕ → Set α),
    s ⊆ iUnion i → ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (i n)

Tactic:
refine fun t ht_subset ↦ iInf_le_of_le t ?_

Goal state after:
case a
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
⊢ ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (t n)
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
· rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
    refine fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_
    calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr

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

Goal state before:
pp: case h.refine_1
x : ℝ
p : EReal × EReal
⊢ p ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1 → ↑x < p.1 * p.2

Tactic:
p_in_prod

Goal state after:
case h.refine_1
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1
⊢ ↑x < p.1 * p.2
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s

Tactic:
have : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
⊢ p ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2) → ↑x < p.1 * p.2

Tactic:
p_in_prod

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)
⊢ ↑x < p.1 * p.2
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, s i)

Tactic:
by
  rw [← iUnion_disjointed]
  exact m.isCaratheodory_iUnion_of_disjoint (m.isCaratheodory_disjointed h)
    (disjoint_disjointed _)

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

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t.Nonempty
⊢ ⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t

Tactic:
by
        simp only [ht, top_apply, le_top]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ f ⟨b, h_b⟩ → a ∈ f ⟨b, h_b⟩

Tactic:
apply id

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ f ⟨b, h_b⟩ → a ∈ f ⟨b, h_b⟩

Tactic:
apply id

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}

Tactic:
rw [piiUnionInter_singleton]

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}
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 γ
s : Set α
t : Set β
⊢ Measurable fun x ↦ (↑x.1, ↑x.2)

Tactic:
fun_prop

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable fun f ↦ (fun c ↦ (f c).1, fun c ↦ (f c).2)

Tactic:
fun_prop

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁶ : MeasurableSpace α✝
inst✝⁵ : MeasurableSpace β✝
inst✝⁴ : MeasurableSpace γ✝
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α : Type u_8
β : Type u_9
γ : Type u_10
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable fun p c ↦ (p.1 c, p.2 c)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set α
ι : Sort u_3
inst✝ : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ i, s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t

Tactic:
by
  simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Nonempty α
hf : MeasurableEmbedding f
⊢ Measurable ⇑hf.equivRange.symm

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ + μ₂ ≪ ν
⊢ μ₁ ≪ ν ∧ μ₂ ≪ ν

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν

Tactic:
· have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0
    exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν : Measure α
h : μ₁ ≪ ν ∧ μ₂ ≪ ν
⊢ ν + ν ≪ ν

Tactic:
rw [← two_smul ℝ≥0]
    exact AbsolutelyContinuous.rfl.smul_left 2

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
this : μ (⋃ n, t n) = ⨆ n, μ (t n)
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
      Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
this : μ (⨆ i, s i) = ⨆ n, Function.extend e (fun x ↦ μ (s x)) (fun x ↦ 0) n
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ - μ s + (μ t + ε) = μ univ - μ s + ε + μ t

Tactic:
add_right_comm,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ - μ s + (μ t + ε) = μ univ - μ s + μ t + ε
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case intro
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
hne : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (⨅ i, μ (⋂ j, ⋂ (_ : j ≤ i), f j)))

Tactic:
exact tendsto_atTop_iInf
    fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij

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
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
⊢ μ (⋃₀ (measurableAtom '' s)) = ν (⋃₀ (measurableAtom '' s))

Tactic:
rw [measure_sUnion h_count h_disj h_meas, measure_sUnion h_count h_disj h_meas]

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
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ t ∈ measurableAtom '' s, MeasurableSet t
⊢ ∑' (s_1 : ↑(measurableAtom '' s)), μ ↑s_1 = ∑' (s_1 : ↑(measurableAtom '' s)), ν ↑s_1
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ (μ.trim hm) s = (Measure.map id μ) s

Tactic:
rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]

Goal state after:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ.inl.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ Disjoint (u' ∩ f n) (v' ∩ f n)

pp: case succ.inl.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' \ f n
⊢ Disjoint (u' ∩ f n) (v' \ f n)

pp: case succ.inr.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' ∩ f n
⊢ Disjoint (u' \ f n) (v' ∩ f n)

pp: case succ.inr.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ Disjoint (u' \ f n) (v' \ f n)

Tactic:
· refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
      exact fun huv' ↦ huv (huv' ▸ rfl)

Goal state after:
case succ.inl.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' \ f n
⊢ Disjoint (u' ∩ f n) (v' \ f n)

case succ.inr.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' ∩ f n
⊢ Disjoint (u' \ f n) (v' ∩ f n)

case succ.inr.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ Disjoint (u' \ f n) (v' \ f n)