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

Goal state before:
pp: case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 ↦ x_1 / x) ∘ u) n ∈ closedBall 0 1
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'

Goal state after:
case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 ↦ x_1 / x) ∘ u) n ∈ closedBall 0 1
a : K
ha' : Tendsto ((fun x_1 ↦ x_1 / x) ∘ u) atTop (𝓝 a)
⊢ ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (P.sup' hP id)

Tactic:
Finset.sup'_eq_sup,

Goal state after:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (P.sup id)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ Measurable f

Tactic:
apply measurable_to_countable'
  rintro (- | -)
  · convert! h.compl
    rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
  exact h

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:
rw [← sUnion_range, measure_sUnion_null_iff (countable_range s), forall_mem_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)

Tactic:
exact MeasurableSet.univ.inr_image

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ ↑(sign x) * |x| = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * |x| = x

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * |0| = 0

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * |x| = x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ |x| * ↑(sign x) = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ |x| * ↑(sign x) = x

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ |0| * ↑(sign 0) = 0

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ |x| * ↑(sign x) = x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ ↑(sign x) * x = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * x = |x|

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * 0 = |0|

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * x = |x|
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ x * ↑(sign x) = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ x * ↑(sign x) = |x|

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ 0 * ↑(sign 0) = |0|

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ x * ↑(sign x) = |x|
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ 1 = sign ↑x✝

Tactic:
sign_pos (EReal.coe_pos.2 h)

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ 1 = 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c

Tactic:
mul_comm a c,

Goal state after:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ b * c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, ← inv_neg, abs_def a,
        coe_ennreal_ofReal, max_eq_left (abs_nonneg a), ← coe_neg |a|, abs_of_neg a_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
      simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
      congr
      exact abs_of_pos a_pos

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (i : α), ENNReal.ofReal (f i) < ∞

Tactic:
unfold ENNReal.ofReal

Goal state after:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (i : α), ↑(f i).toNNReal < ∞
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)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN : dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Tactic:
dist_nndist,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN : ↑(nndist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x)) < ↑ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
⊢ ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
(hb : (∑' i, μ (s i)) < ∞)

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥

Tactic:
rw [limsup_bot]; exact bot_le

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

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

Tactic:
funext n

Goal state after:
case e'_5
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
· simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩

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

Goal state before:
pp: k : ℕ
hn : 0 < k.succ
⊢ ↑k.succ ! / ↑k.succ ^ k.succ ≤ 1 / ↑k.succ

Tactic:
rw [factorial_eq_prod_range_add_one, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
        Finset.prod_range_succ']

Goal state after:
k : ℕ
hn : 0 < k.succ
⊢ (∏ k_1 ∈ Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x

Tactic:
refine ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x → ContinuousWithinAt f s x
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
⊢ (∃ n, dissipate s n = ∅) ↔ ∃ n, s n = ∅

Tactic:
by
  refine ⟨?_, fun ⟨n, hn⟩ ↦ ⟨n, subset_eq_empty (dissipate_subset le_rfl) hn⟩⟩
  contrapose!
  intro h n
  obtain ⟨m, hm⟩ := exists_subset_dissipate_of_directed hd n
  exact (h m).mono hm

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : Set α
h : m.IsCaratheodory sᶜ
⊢ m.IsCaratheodory s

Tactic:
simpa using isCaratheodory_compl m h

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x ∈ Finset.range n, m (s x) = m (⋃ i, ⋃ (_ : i < n), s i)
⊢ m (⋃ i, ⋃ (_ : i < n), s i) ≤ m (⋃ i, s i)

Tactic:
exact m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : 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)
⊢ ∀ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
· intro b h_b
    simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
      at h_b
    obtain ⟨h_b_w, h_b_h⟩ := h_b
    have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
    rw [h_b_alt, Subtype.val_injective.extend_apply]
    apply h_t'
    apply h_b_h

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ (fun i ↦ m (f i) ⋯) = fun i ↦ (inducedOuterMeasure m ⋯ m0) (f i)

Tactic:
funext n

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
n : ℕ
⊢ m (f n) ⋯ = (inducedOuterMeasure m ⋯ m0) (f n)
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) ⋯
⊢ ∀ (t : Set α) (ht : MeasurableSet t), C t ht

Tactic:
have eq : MeasurableSet = DynkinSystem.GenerateHas s := by
    rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
    rfl
  suffices ∀ t (ht : DynkinSystem.GenerateHas s t), C t (eq ▸ ht) from
    fun t ht ↦ this t (eq ▸ ht)
  intro t ht
  induction ht with
  | basic u hu => exact basic u hu
  | empty => exact empty
  | @compl u hu ihu => exact compl _ (eq ▸ hu) ihu
  | @iUnion f hfd hf ihf => exact iUnion f hfd (eq ▸ hf) ihf

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂

Tactic:
refine le_iInf ?_; intro h₂
  have :=
    extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁
      (h₂.diff h₁)
  rw [union_sdiff_cancel hs] at this
  rw [← extend_eq m]
  exact le_iff_exists_add.2 ⟨_, this⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ m (disjointed f i) ⋯ ≤ m (f i) ⋯

Tactic:
← extend_eq m,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ extend m (disjointed f i) ≤ m (f i) ⋯
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_5
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Monotone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, s i)

Tactic:
by
  cases isEmpty_or_nonempty ι with
  | inl _ => simp
  | inr _ => exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
intro r hs

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ms ≤ m (⋂ n, t n)

Tactic:
refine iInf_le_of_le (⋂ n, t n) ?_
      refine iInf_le_of_le (subset_iInter hsub) ?_
      exact iInf_le _ (MeasurableSet.iInter hm)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Tactic:
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩

Goal state after:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᵐ[μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : ¬AEMeasurable f μ
⊢ map f μ = map g μ

Tactic:
have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : ¬AEMeasurable f μ
hg : ¬AEMeasurable g μ
⊢ map f μ = map g μ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
s : Set α
hs : MeasurableSet s
⊢ μ s = ν s

Tactic:
rw [← Set.preimage_image_eq s hf.injective, ← hf.map_apply, ← hf.map_apply]

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
h : map f μ = map f ν
s : Set α
hs : MeasurableSet s
⊢ (map f μ) (f '' s) = (map f ν) (f '' s)
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
hs : NullMeasurableSet s (comap f μ)
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s) μ

Tactic:
exact hf _ (measurableSet_toMeasurable _ _)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ (s ∩ t).Nonempty

Tactic:
← Set.not_disjoint_iff_nonempty_inter

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ ¬Disjoint s t
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.restrict s = 0 ↔ μ s = 0

Tactic:
by
  rw [← measure_univ_eq_zero, restrict_apply_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
⊢ μ ((⋂ n, w n) ∩ u) ≤ μ (t ∩ u)

Tactic:
hμ,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
⊢ (sum m) ((⋂ n, w n) ∩ u) ≤ (sum m) (t ∩ u)
Module: Mathlib.MeasureTheory.Measure.Trim

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

Tactic:
Set.preimage_id

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ μ s = μ s
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
⊢ memPartitionSet f n a = s ↔ a ∈ s

Tactic:
refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩
  by_contra h_ne
  have h_disj : Disjoint s (memPartitionSet f n a) :=
    disjoint_memPartition f n hs (memPartitionSet_mem f n a) (Ne.symm h_ne)
  refine absurd h_disj ?_
  rw [not_disjoint_iff_nonempty_inter]
  exact ⟨a, h, mem_memPartitionSet f n a⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (t ∩ u)) univ = μ (t ∩ u)

Tactic:
rw [restrict_apply MeasurableSet.univ, univ_inter]

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₁

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))

Tactic:
rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map f (ae (μ.restrict s)) → t ∈ Filter.map f (ae (μ.restrict s))
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
s : Set β
hs : s ∈ S
⊢ MeasurableSet (Subtype.val '' f ∘ Subtype.val ⁻¹' s)

Tactic:
rw [preimage_comp, Subtype.image_preimage_coe]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
a✝ : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
T : Set β → Set α
hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s
hTm : ∀ s ∈ S, MeasurableSet (T s)
hTeq : ∀ s ∈ S, T s =ᵐ[μ] f ⁻¹' s
U : Set β → Set α
hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s
hUm : ∀ s ∈ S, MeasurableSet (U s)
hUeq : ∀ s ∈ S, U s =ᵐ[μ] f ⁻¹' s
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : μ v = 0
s : Set β
hs : s ∈ S
⊢ MeasurableSet (vᶜ ∩ f ⁻¹' s)