mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.support = univ ↔ L.filter ≤ atTop

Tactic:
by
  simp only [support, Set.eq_univ_iff_forall, Set.mem_ofPred]
  refine ⟨fun h s hs ↦ ?_, fun h b ↦ .filter_mono h ?_⟩
  · obtain ⟨t, ht⟩ := mem_atTop_sets.mp hs
    have := (Filter.biInter_finset_mem t).mpr fun b hb ↦ h b
    exact Filter.mem_of_superset this fun r hr ↦ ht r (by simpa using! hr)
  · filter_upwards [eventually_ge_atTop {b}] using by simp

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
⊢ (∀ᶠ (s : Finset β) in L.filter, b ∈ s) ∨ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

Tactic:
rw [or_iff_not_imp_left]

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
⊢ (¬∀ᶠ (s : Finset β) in L.filter, b ∈ s) → ∀ᶠ (s : Finset β) in L.filter, b ∉ s
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
hAtTop : atTop = pure Finset.univ
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hL : { filter := F }.filter ≤ atTop
hL' : ∅ ∉ { filter := F }.filter
⊢ { filter := F } = unconditional β

Tactic:
| mk F =>

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ ∃ᶠ (i : R) in F, f i ≤ f m

Tactic:
apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ ∀ (x : R), m < x → f x ≤ f m
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst✝ : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
hs : ↑s ⊆ L.support
⊢ ∀ x ∈ s, x ∉ Set.range g → f x = 1

Tactic:
exact fun x h h' ↦ hf x (hs h) h'

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b

Tactic:
have hv := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_right _ _) hb) h₄

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr.inr.e_u
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ (fun a ↦ s.sup fun i ↦ F i a) = fun a ↦ s.sup' s_nemp fun i ↦ F i a

Tactic:
ext a

Goal state after:
case inr.inr.e_u
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
a : α
⊢ (s.sup fun i ↦ F i a) = s.sup' s_nemp fun i ↦ F i a
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
⊢ ∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (b : β), m (s b)

Tactic:
rw [← tprod_extend_one (@encode_injective β _)]

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
⊢ ∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (y : ℕ), extend encode (fun b ↦ m (s b)) 1 y
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Goal state after:
case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
n : ℕ
⊢ ¬Multipliable fun k ↦ f (k + n)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
SemiconjBy,

Goal state after:
case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : Summable f L
⊢ (∑'[L] (i : ι), f i) * a = b * ∑'[L] (i : ι), f i
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
inst✝¹ : T2Space α
inst✝ : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
⊢ SemiconjBy a (∑'[L] (i : ι), f i) (∑'[L] (i : ι), g i)

Tactic:
SemiconjBy,

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
inst✝¹ : T2Space α
inst✝ : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
⊢ a * ∑'[L] (i : ι), f i = (∑'[L] (i : ι), g i) * a
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
by
  simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
  exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (range f) = Metric.diam univ

Tactic:
by
  rw [← image_univ]
  exact hf.diam_image univ

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ⇑h '' Metric.eball x r = Metric.eball (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_eball, symm_symm]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
x : ℕ → X
inst✝¹ : SequentialSpace X
inst✝ : T1Space X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst✝²] (range x)

Tactic:
simpa using isClosed_iUnion_closure_singleton_of_not_tendsto hx

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

Goal state before:
pp: case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
⊢ 0 < ε → ∃ n, f n < ε

Tactic:
hε

Goal state after:
case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n < ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
⊢ 0 < ε → ∃ n, f n ≤ ε

Tactic:
hε

Goal state after:
case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε < ε * 2

Tactic:
conv_lhs => rw [← mul_one ε]

Goal state after:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε * 1 < ε * 2
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
⊢ IsClosed[Pi.topologicalSpace] {f | LipschitzWith K f}

Tactic:
by
  simp only [← lipschitzOnWith_univ, isClosed_setOfPred_lipschitzOnWith]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
⊢ ∀ {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n

Tactic:
n

Goal state after:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
⊢ (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
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 α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
⊢ ε > 0 →
    ∃ δ > 0,
      ∀ x ∈ s,
        ∀ y ∈ s,
          dist x y ≤ δ → dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) x) (Function.uncurry (fun x1 x2 ↦ x1 • x2) y) ≤ ε

Tactic:
hε

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ x ∈ s,
      ∀ y ∈ s,
        dist x y ≤ δ → dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) x) (Function.uncurry (fun x1 x2 ↦ x1 • x2) y) ≤ ε
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

Tactic:
simpa using norm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
x y : β
⊢ ‖s • x - s • y‖ = ‖s‖ * ‖x - y‖

Tactic:
(norm_smul s (x - y)).symm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
x y : β
⊢ ‖s • x - s • y‖ = ‖s • (x - y)‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖

Tactic:
by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
⊢ ε > 0 → ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
hε

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
by_cases b ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
⊢ s = (s.indicator fun x ↦ b) ⁻¹' {0}ᶜ

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
a : α
⊢ a ∈ s ↔ a ∈ (s.indicator fun x ↦ b) ⁻¹' {0}ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x ↦ b)
⊢ MeasurableSet s

Tactic:
convert! h (MeasurableSet.singleton (0 : β)).compl
    ext a
    simp [NeZero.ne b]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s = ∅
⊢ ⊤ s = ⨅ (_ : s = ∅), 0

Tactic:
by simp [h]

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

Goal state before:
pp: ⊢ EReal.abs 0 = 0

Tactic:
by rw [abs_eq_zero_iff]

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

Goal state before:
pp: x : ℝ
⊢ ↑(ENNReal.ofReal |x|) = ↑|x|

Tactic:
← Real.coe_nnabs,

Goal state after:
x : ℝ
⊢ ↑(ENNReal.ofReal ↑(Real.nnabs x)) = ↑↑(Real.nnabs x)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ sign ↑x = sign x

Tactic:
by
  simp only [sign, OrderHom.coe_mk, EReal.coe_pos, EReal.coe_neg']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
⊢ (∀ (x : α), UpperHemicontinuousAt f x) ↔
    ∀ (x : α) (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
upperHemicontinuousAt_iff_frequently

Goal state after:
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
⊢ 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
hε

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 < ε
⊢ ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ Tendsto toReal (𝓝[≠] ⊥) atBot

Tactic:
nhdsWithin_bot,

Goal state after:
⊢ Tendsto toReal (map Real.toEReal atBot) atBot
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f

Tactic:
by
  obtain rfl | h₃ := h₁.eq_or_lt
  · simp
  simp_rw [EReal.mul_comm (x := c)]
  apply eq_of_le_of_ge
  · rw [limsup_le_iff]
    simpa [← EReal.lt_div_iff (by aesop) (by aesop)]
      using fun _ ↦ eventually_lt_of_limsup_lt
  · rw [le_limsup_iff]
    simpa [← EReal.div_lt_iff (by aesop) (by aesop)]
      using fun _ ↦ frequently_lt_of_lt_limsup

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : ExistsAddOfLE α
inst✝ : Archimedean α
r : α
h : 1 < r
⊢ Tendsto (fun n ↦ r ^ n) atTop atTop

Tactic:
by
  obtain ⟨r, r0, rfl⟩ := exists_pos_add_of_lt' h
  rw [add_comm]
  exact tendsto_add_one_pow_atTop_atTop_of_pos r0

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
⊢ ∀ (n : ℕ), (dissipate s n).Nonempty

Tactic:
n

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
n : ℕ
⊢ (dissipate s n).Nonempty
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
⊢ IsPiSystem (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
rintro _ ⟨s₁, hs₁, t₁, ht₁, rfl⟩ _ ⟨s₂, hs₂, t₂, ht₂, rfl⟩ hst

Goal state after:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : ((fun x1 x2 ↦ x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 ↦ x1 ×ˢ x2) s₂ t₂).Nonempty
⊢ (fun x1 x2 ↦ x1 ×ˢ x2) s₁ t₁ ∩ (fun x1 x2 ↦ x1 ×ˢ x2) s₂ t₂ ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: 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 ∅

Tactic:
ext a

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
a : α
⊢ a ∈ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ↔
    a ∈ ⋂ 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 ∅
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

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

Tactic:
exact m.isCaratheodory_iUnion_of_disjoint (m.isCaratheodory_disjointed h)
    (disjoint_disjointed _)

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)
⊢ ⋂ b ∈ T, f b = ⋂ b ∈ Finset.image (fun x ↦ ↑x) T, Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b

Tactic:
ext a

Goal state after:
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
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:
rw [measure_eq_extend (MeasurableSet.iUnion h),
    extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
  · simp [measure_eq_extend, h]
  · exact μ.empty
  · exact μ.m_iUnion

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
by_cases h : AEMeasurable f μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

case neg
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : ¬AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
⊢ μ s = 0

Tactic:
rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
t : Set α
h1t : s ⊆ t
h2t : MeasurableSet t
h3t : ν t = 0
⊢ μ s = 0