mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_2
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2} = univ

pp: case refine_3
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, μ s_1 ≠ ∞

pp: case refine_4
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l ≤ u ∧ Icc l u = S}, μ s = ν s

Tactic:
· refine sUnion_eq_univ_iff.2 fun x => ?_
    rcases hsd.exists_le' hsb x with ⟨l, hls, hlx⟩
    rcases hsd.exists_ge' hst x with ⟨u, hus, hxu⟩
    exact ⟨_, ⟨l, hls, u, hus, hlx.trans hxu, rfl⟩, hlx, hxu⟩

Goal state after:
case refine_3
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}, μ s_1 ≠ ∞

case refine_4
α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
s : Set α
hsc : s.Countable
hsd : Dense s
hsb : ∀ (x : α), IsBot x → x ∈ s
hst : ∀ (x : α), IsTop x → x ∈ s
this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i ≤ i_2), x = Icc i i_2}.Countable
⊢ ∀ s ∈ {S | ∃ l u, l ≤ u ∧ Icc l u = S}, μ s = ν s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_5
m : MeasurableSpace α
inst✝ : CountablySeparated α
⊢ ∃ x, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
  rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩
  exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s

Tactic:
← Finset.mem_coe,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ ↑(f.restrict s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ⇑f '' s
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < b ∨ ∃ d < c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a, (a < b ∨ ∃ d < c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : Add α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a, (a < b ∨ ∃ d ≤ c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < c ∨ ∃ d < b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a, (a < c ∨ ∃ d < b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftMono α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a, (a < c ∨ ∃ d ≤ b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)

Tactic:
aesop

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

Goal state before:
pp: case e'_2
q : ℚ
⊢ Rat.cast '' {x | q < x} = Ioi ↑q ∩ range Rat.cast

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)

Tactic:
aesop

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y

Tactic:
(«tacticBy_cases_:_»
 "by_cases"
 [`hy ":"]
 («term_∈_»
  `y
  "∈"
  (Set.«term_⁻¹'_»
   `f
   "⁻¹'"
   (choice
    («term{_}» "{" [`x] "}")
    (Term.structInst
     "{"
     []
     (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
     (Term.optEllipsis [])
     []
     "}")))))

Goal state after:
case pos
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y

case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (g + piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) y
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case insert
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥

Tactic:
(«tacticBy_cases_:_»
 "by_cases"
 [`hy ":"]
 («term_∈_»
  `y
  "∈"
  (Set.«term_⁻¹'_»
   `f
   "⁻¹'"
   (choice
    («term{_}» "{" [`x] "}")
    (Term.structInst
     "{"
     []
     (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
     (Term.optEllipsis [])
     []
     "}")))))

Goal state after:
case pos
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥

case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y

Tactic:
(«tacticBy_cases_:_»
 "by_cases"
 [`hy ":"]
 («term_∈_»
  `y
  "∈"
  (Set.«term_⁻¹'_»
   `f
   "⁻¹'"
   (choice
    («term{_}» "{" [`x] "}")
    (Term.structInst
     "{"
     []
     (Term.structInstFields [(Term.structInstField (Term.structInstLVal `x []) [])])
     (Term.optEllipsis [])
     []
     "}")))))

Goal state after:
case pos
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y

case neg
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ f y = (piecewise (⇑f ⁻¹' {x})ᶜ ⋯ g (SimpleFunc.const α x)) y
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case hnhds
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
rintro ⟨x, y⟩ -

Goal state after:
case hnhds
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
x : X
y : Y
⊢ ∃ t ∈ 𝓝[K] (x, y), ∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : μ sᶜ = 0
a✝ : Nontrivial α
a x : α
hx : x ∈ s
⊢ x ∈ {x | (fun x ↦ id x = (closure[inst✝²] s).piecewise id (fun x ↦ a) x) x}

Tactic:
by simp [subset_closure hx]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ s.indicator f =ᵐ[μ] s.indicator (AEStronglyMeasurable.mk f h)

Tactic:
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (h.mk f) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEStronglyMeasurable.mk f h)
⊢ s.indicator f =ᵐ[μ] s.indicator (AEStronglyMeasurable.mk f h)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

Tactic:
have : ∀ᵐ x ∂μ, x ∉ t := measure_eq_zero_iff_ae_notMem.1 ht0

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x | (fun a ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : μ t = 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (a : α), ⨆ n, (⇑(eapprox f n) + ⇑(eapprox g n)) a ∂μ = ⨆ n, (eapprox f n).lintegral μ + (eapprox g n).lintegral μ

Tactic:
lintegral_iSup

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, ∫⁻ (a : α), (⇑(eapprox f n) + ⇑(eapprox g n)) a ∂μ = ⨆ n, (eapprox f n).lintegral μ + (eapprox g n).lintegral μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∀ (n : ℕ), Measurable (⇑(eapprox f n) + ⇑(eapprox g n))

case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ Monotone fun n ↦ ⇑(eapprox f n) + ⇑(eapprox g n)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
f : α → ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ ∫⁻ (x : α) in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ (x : α) in s i, f x ∂μ

Tactic:
by
  simp only [lintegral_def, iSup_comm (ι := ι),
    SimpleFunc.lintegral_restrict_iUnion_of_directed _ hd]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), ⨆ n, (const α r * eapprox f n) a ∂μ = ⨆ n, r * (eapprox f n).lintegral μ

Tactic:
lintegral_iSup

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ∫⁻ (a : α), (const α r * eapprox f n) a ∂μ = ⨆ n, r * (eapprox f n).lintegral μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable ⇑(const α r * eapprox f n)

case h_mono
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Monotone fun n ↦ ⇑(const α r * eapprox f n)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)) (f (e n)) < ∞

Tactic:
simp only [Nat.pairEquiv_symm_apply, measure_union_lt_top_iff, f, e]
    rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT', Set.compl_inter_self,
      Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT']
    simp only [measure_empty, ENNReal.zero_lt_top, true_and]
    refine (measure_mono Set.inter_subset_left).trans_lt ?_
    rw [← Measure.restrict_apply' (measurableSet_sigmaFiniteSetGE _)]
    exact measure_spanningSets_lt_top _ _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

Tactic:
refine
    @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s → ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ

case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ →
            ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ →
              ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Perfect C
x : α
xC : x ∈ C
xU : x ∈ U
Uop : IsOpen[inst✝] U
⊢ Perfect (closure[inst✝] (U ∩ C)) ∧ (closure[inst✝] (U ∩ C)).Nonempty

Tactic:
constructor
  · apply Preperfect.perfect_closure
    exact hC.acc.open_inter Uop
  apply Nonempty.closure
  exact ⟨x, ⟨xU, xC⟩⟩

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

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
⊢ ∀ a ∉ Finite.toFinset hN, ‖f a x‖ ≤ u a

Tactic:
aesop

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
intro n m N hn hm
    have A n : u n ∈ s := h'u (mem_range_self _)
    apply (hf.dist_le_mul _ (A n) _ (A m)).trans
    exact mul_le_mul_of_nonneg_left (hb n m N hn hm) K.2

Goal state after: