mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ rs ↑⟨n, hn⟩ ≤ ⨆ n, rs ↑n

Tactic:
by
      refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
      have : Finite {n | b'' < u n r} := by simpa using! hb''
      exact Finite.bddAbove_range _

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

Goal state before:
pp: a b : EReal
⊢ a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
by
  rw [ne_eq, mul_eq_bot]
  push +distrib Not
  rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ (if L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite then ∏ᶠ (b : β), f b
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
rw [eq_true_intro hf, if_pos]

Goal state after:
case pos.hc
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ L.HasSupport ∧ True
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
⊢ limsup (fun x ↦ g (u x)) f ≤ g (limsup u f)

Tactic:
rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
⊢ g (g.symm (limsup (fun x ↦ g (u x)) f)) ≤ g (limsup u f)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝ : L.LeAtTop
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L

Tactic:
by
  simpa [prod_attach, Embedding.subtype] using Finset.hasProd_support s f L

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst✝ : L.LeAtTop
this : HasProd f (∏ b' ∈ {b}, f b') L
⊢ HasProd f (f b) L

Tactic:
simpa using this

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Tactic:
by
  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

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

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ (fun i ↦ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' (k : ℕ), f (k + i)

Tactic:
ext1 i

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j = ∏' (k : ℕ), f (k + i)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
· simp [hn]

Goal state after:
case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
· simp [hn]

Goal state after:
case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : IsEmpty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

pp: case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
· simp [hn]

Goal state after:
case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
V : Set (X × X)
⊢ V ∈ 𝓤 X → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}

Tactic:
V_in

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F✝ : Type u_5
G : Type u_6
F : Type u_7
inst✝ : NormedGroup F
⊢ ‖1‖ₑ = 0

Tactic:
simp [enorm_eq_nnnorm]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F✝ : Type u_5
G : Type u_6
F : Type u_7
inst✝ : NormedGroup F
⊢ ∀ (x : F), ‖x‖ₑ = 0 ↔ x = 1

Tactic:
simp [enorm_eq_nnnorm]

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

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
h : ∀ i ∈ ∅, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ ∅, a i ≠ ∞
⊢ Tendsto (fun b ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))

Tactic:
simp [tendsto_const_nhds]

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

Goal state before:
pp: x y : ℝ≥0∞
hp : ¬(x = ∞ ∧ y = ∞)
⊢ ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} (x, y)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))

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

Goal state before:
pp: β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist a ↑x + edist a ↑y < r + r

Tactic:
edist_comm a x,

Goal state after:
β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist (↑x) a + edist a ↑y < r + r
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x ↦ f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i ↦ g i x) x

Tactic:
ext1 i

Goal state after:
case refine_2
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x ↦ f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i ↦ g i x) x i
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (fun a ↦ max (dist (f a) 0) (dist (g a) 0)) (𝓝[s] x), (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ Tendsto (fun y ↦ ((f • g) y.2, (F • G) y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
simp_rw [Filter.eventually_map, max_le_iff] at hC

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
⊢ Tendsto (fun y ↦ ((f • g) y.2, (F • G) y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∀ y ∈ Set.range fun n ↦ ‖u n‖, y ≤ C + ‖u 0‖

Tactic:
simpa using this

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ⋯.choose ≠ 0

Tactic:
exact (DilationClass.edist_eq' f).choose_spec.1

Goal state after:
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y ≠ ∞ → y ≠ ∞

Tactic:
rintro h rfl

Goal state after:
x : ℝ≥0
hx : x ≠ 0
h : x • ∞ ≠ ∞
⊢ False
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ z ⟨i, hit⟩ = (piFinsetUnion π hst) (y, z) ⟨i, ⋯⟩

Tactic:
exact piCongrLeft_sumInr (fun b : ↥(s ∪ t) => π b) e y z ⟨i, hit⟩ |>.symm

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ (closedBall x (‖x‖ / 2))ᶜ ∈ 𝓝 0

pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ closedBall x (‖x‖ / 2) ∈ 𝓝 x

Tactic:
· refine Metric.isClosed_closedBall.isOpen_compl.mem_nhds ?_
      simpa

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ closedBall x (‖x‖ / 2) ∈ 𝓝 x
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})

Tactic:
exact .biUnion hs fun b _ => .singleton b

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ ‖-x + x‖ = 0

Tactic:
simp only [add_comm, ← sub_eq_add_neg, sub_self]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
⊢ ‖0‖ = 0
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:
← smul_one_mul c,

Goal state after:
α : 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 • 1 * m s ≤ c • m t
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.16
f : α → β
m : OuterMeasure α
s : ℕ → Set β
x✝ : Pairwise (Disjoint on s)
⊢ m (f ⁻¹' ⋃ i, s i) ≤ ∑' (i : ℕ), m (f ⁻¹' s i)

Tactic:
simpa using measure_iUnion_le fun i => f ⁻¹' s i

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Nonempty
a : α
as : a ∈ s
⊢ ∞ ≤ (∞ • dirac a) s

Tactic:
by simp [as]

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x ↦ g x a

Tactic:
measurable_iff_comap_le,

Goal state after:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ MeasurableSpace.comap g MeasurableSpace.pi ≤ inst✝¹ ↔
    ∀ (a : δ), MeasurableSpace.comap (fun x ↦ g x a) (inst✝ a) ≤ inst✝¹
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)
  refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_
  rw [sum_Ico_eq_sum_range]
  refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_
  exact hd.comp_injective (add_right_injective n)

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

Goal state before:
pp: a : SignType
⊢ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
by
  cases a <;> simp

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

Goal state before:
pp: case inl.a
hz : Odd 0
⊢ False

Tactic:
simp at hz

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

Goal state before:
pp: case pos
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
simp [hf]

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i

Tactic:
· exact fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset_range.2 hst)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
x : α
hx : r x = r' x
⊢ r x b → r' x b

Tactic:
hxb

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
x : α
hx : r x = r' x
hxb : r x b
⊢ r' x b
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ n * u 0 ≤ u n

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h

Goal state after:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ ∀ k < n, c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_1
r : ℝ≥0∞
⊢ r ≤ 1 → ¬Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
intro r_le_one h_tends

Goal state after:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)
⊢ False
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯) s ≤ ((comap f) (OuterMeasure.ofFunction m m_empty)) s

Tactic:
· rw [comap_apply, ofFunction_apply, ofFunction_apply]
    refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩
    refine iInf_mono' fun ht => ?_
    rw [Set.image_subset_iff, preimage_iUnion] at ht
    refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩
    rcases h with hl | hr
    exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
⊢ (comap f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯

Tactic:
by
  refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_
  · rw [comap_apply]
    apply ofFunction_le
  · rw [comap_apply, ofFunction_apply, ofFunction_apply]
    refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩
    refine iInf_mono' fun ht => ?_
    rw [Set.image_subset_iff, preimage_iUnion] at ht
    refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩
    rcases h with hl | hr
    exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))

Tactic:
rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)

Goal state after:
case inl
α : Type u_1
inst✝ : PseudoMetricSpace α
r : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n ↦ 0 * r ^ n) (0 / (1 - r))

case inr
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n ↦ C * r ^ n) (C / (1 - r))
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s ↦ m (f '' s)

Tactic:
dsimp only [boundedBy]

Goal state after:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ =
    OuterMeasure.ofFunction (fun s ↦ ⨆ (_ : s.Nonempty), m (f '' s)) ⋯
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty ↑I
⊢ (restrict s) (⨅ i, m ↑i) = ⨅ i, (restrict s) (m ↑i)

Tactic:
exact restrict_iInf _ _

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S

pp: case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
· simp [ht]

Goal state after:
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case inter
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty✝ : (s✝ ∩ t✝).Nonempty
h_s : MeasurableSet s✝
h_u : MeasurableSet t✝
⊢ MeasurableSet (s✝ ∩ t✝)

Tactic:
apply MeasurableSet.inter h_s h_u

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

Goal state before:
pp: case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

pp: case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
· simp [ht]

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

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

Tactic:
measure_eq_extend (MeasurableSet.iUnion h),

Goal state after:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ extend (fun t _ht ↦ μ t) (⋃ b, f b) = ∑' (i : ι), μ (f i)
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
hb' : b' < toDual a
⊢ ∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Tactic:
simpa [OrderDual.exists] using hs (ofDual b') hb'

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
b : ι
⊢ NullMeasurableSet (M (t b) ∩ M (⋃ b, s b)) μ

pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≠ ∞

Tactic:
· measurability

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ∞
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

Tactic:
by
  rw [restrict_apply' hs]

Goal state after: