mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

Tactic:
constructor

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

Tactic:
constructor

Goal state after:
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1

Tactic:
constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1

Tactic:
constructor

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0

Tactic:
constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1

Tactic:
constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

Tactic:
constructor

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0

Tactic:
constructor

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

Goal state before:
pp: x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y ↔ x = y

Tactic:
constructor

Goal state after:
case mp
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y → x = y

case mpr
x y : EReal
⊢ x = y → x.abs = y.abs ∧ sign x = sign y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ x ≤ y ↔
    sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

Tactic:
constructor

Goal state after:
case mp
x y : EReal
⊢ x ≤ y →
    sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

case mpr
x y : EReal
⊢ sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs →
    x ≤ y
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
h : Summable fun a ↦ ↑(f a)
⊢ (support f).Countable

Tactic:
simpa [support] using h.countable_support

Goal state after:
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

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

case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ (-⊤)⁻¹ = -⊤⁻¹

Tactic:
rw [neg_top, inv_bot, inv_top, neg_zero]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f ↔ (∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f → (∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩

case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ ((∀ (x : α), Summable fun y ↦ f ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩) → Summable f
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
⊢ {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
x✝ : α × β
⊢ x✝ ∈ {x | x.2 ∈ f x.1 ∩ g x.1} ↔ x✝ ∈ {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
Module: Mathlib.Data.EReal.Inv

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

Tactic:
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.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 :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f N) (f n) < ↑ε

Tactic:
refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_

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 :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ ∑ i ∈ Finset.Ico N n, ↑(d i) < ↑ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)

case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x
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
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) ↔
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

Tactic:
constructor

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

case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1) →
    ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓝 0)

Tactic:
by
  convert! NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜
  simp

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

Goal state before:
pp: case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)

Tactic:
have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [mul_zero, add_zero, div_one]

Goal state after:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n ↦ 1 / (1 + x / ↑n)) atTop (𝓝 1)
Module: Mathlib.Topology.Semicontinuity.Basic

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

Tactic:
by
  rw [lowerSemicontinuousWithinAt_iff, inv_surjective.forall, upperSemicontinuousWithinAt_iff]
  simp

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✝ : OrderTopology γ
f : α → γ
⊢ ContinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f

Tactic:
continuousOn_iff_lower_upperSemicontinuousOn,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuousOn f univ ∧ UpperSemicontinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)

Tactic:
by exact Icc_inter_Icc

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst✝ : LinearOrder α
f : ι → α
g : ι' → α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)

Tactic:
by exact Icc_inter_Icc

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case h
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b =
      ⋂ b ∈ T_s ∪ T_t',
        (fun b ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∧
    ∀ b ∈ T_s ∪ T_t',
      (fun b ↦ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) b ∈ g b

Tactic:
constructor

Goal state after:
case h.left
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b =
    ⋂ b ∈ T_s ∪ T_t', if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅

case h.right
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
⊢ ∀ b ∈ T_s ∪ T_t',
    (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
⊢ MeasurableSet s

Tactic:
apply ofFunction_caratheodory; intro t
  rcases t.eq_empty_or_nonempty with rfl | h
  · simp [Set.not_nonempty_empty]
  · convert! le_trans _ (hs t)
    · simp [h]
    exact add_le_add iSup_const_le iSup_const_le

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

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

Tactic:
constructor

Goal state after:
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 : α
⊢ a ∈ ⋂ b ∈ T, f b → a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

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 : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b → a ∈ ⋂ b ∈ T, f b
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ (fun i ↦ ⋃ (_ : i ∈ s), f i) = fun i ↦ ⋃ (_ : i ∈ hs.toFinset), f i

Tactic:
ext

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
x✝¹ : β
x✝ : α
⊢ x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹ ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ hs.toFinset), f 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
s : Set α
⊢ sᶜ ∈ ae μ ↔ μ s = 0

Tactic:
by simp only [mem_ae_iff, compl_compl]

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

Tactic:
constructor

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

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ (∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ) → AEMeasurable g μ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

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

Tactic:
constructor

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

case mpr
α : Type u_1
s t : Set α
⊢ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ → ∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
⊢ (f ⊓ g).IsMeasurablyGenerated

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
⊢ ∀ ⦃s : Set α⦄, s ∈ f ⊓ g → ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ s
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∃ᶠ (i : ι) in atTop, MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
by
  rw [← compl_iff, compl_iInter]
  exact .iUnion_of_monotone_of_frequently (compl_anti.comp hsm) <| hs.mono fun _ ↦ .compl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ✝ ν : Measure α
s✝ : Set α
inst✝ : MeasurableSpace β
f : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure β
hf : ∀ (μ : Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory
c : ℝ≥0∞
μ : Measure α
s : Set β
hs : MeasurableSet s
⊢ ((f (c • μ).toOuterMeasure).toMeasure ⋯) s = ((RingHom.id ℝ≥0∞) c • (f μ.toOuterMeasure).toMeasure ⋯) s

Tactic:
simp only [map_smulₛₗ, Pi.smul_apply, toMeasure_apply, smul_toOuterMeasure (R := ℝ≥0∞),
      FunLike.coe_smul, smul_apply, hs]

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop ↔ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
constructor

Goal state after:
case pos.mp
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
⊢ comap Subtype.val (𝓝[<] b) = atTop → ∀ a < b, (s ∩ Ioo a b).Nonempty

case pos.mpr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
⊢ (∀ a < b, (s ∩ Ioo a b).Nonempty) → comap Subtype.val (𝓝[<] b) = atTop
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inr
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ n ∈ Icc a_L a_R

Tactic:
constructor

Goal state after:
case inr.left
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ a_L ≤ n

case inr.right
X : Type u_1
inst✝⁶ : LinearOrder X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : OrderTopology X
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoMaxOrder X
inst✝ : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h✝ : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ n ≤ a_R
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (map f μ)

Tactic:
constructor

Goal state after:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ (map f μ) univ < ∞
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case As_mble
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)

Tactic:
exact fun i ↦ (As_mble i).mono (le_sum _ _)

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

Goal state before:
pp: α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
⊢ IsFiniteMeasure ν

Tactic:
constructor

Goal state after:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
hs : MeasurableSet s
⊢ ν univ < ∞