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

Goal state before:
pp: case a
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
⊢ liminf f F ≤ f F.limsSup

Tactic:
by_cases! h' : ∃ c, c < F.limsSup ∧ Set.Ioo c F.limsSup = ∅

Goal state after:
case pos
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 = ∅
⊢ liminf f F ≤ f F.limsSup

case neg
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
⊢ liminf f F ≤ f F.limsSup
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

pp: case neg
α : 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]
    simp only [and_true]
    infer_instance

Goal state after:
case neg
α : 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
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
x✝¹ : { x // x ∈ t }
x✝ : x✝¹ ∈ t'
⊢ ?m.138 ↑x✝¹ = f ↑x✝¹

Tactic:
by rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
this : update f i 1 ≤ update g i 1
⊢ a₁ < a₂

Tactic:
have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
this✝ : update f i 1 ≤ update g i 1
this : 1 / f i * a₁ ≤ 1 / g i * a₂
⊢ a₁ < a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
⊢ Summable (fun i ↦ f i / a) L ↔ Summable f L

Tactic:
by
  simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: x y z : ℝ
h : y ∈ uIcc x z
⊢ dist x y ≤ dist x z

Tactic:
by
  simpa only [dist_comm x] using! abs_sub_left_of_mem_uIcc h

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

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
simp only [← summable_coe, ← tendsto_coe] at hf ⊢

Goal state after:
α : Type u_3
f : α → ℝ≥0
hf : Summable fun a ↦ ↑(f a)
⊢ Tendsto (fun a ↦ ↑(f a)) cofinite (𝓝 ↑0)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : EMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y

Tactic:
by
  simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y

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

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ lxy.length + 1 = (lxy ++ [y]).length

Tactic:
length_append,

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ lxy.length + 1 = lxy.length + [y].length
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure[inst✝²] s
⊢ x ∈ seqClosure s

Tactic:
rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)

Tactic:
nth_rewrite 2 [← coe_toNNReal ha]

Goal state after:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 ↑a.toNNReal)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : l < ∞), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ∞), 𝓟 (Ioi a)

Tactic:
by simp [lt_top_iff_ne_top, Ioi]

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

Goal state before:
pp: case refine_2.zero
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ v 0 ∈ s

pp: case refine_2.succ
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n✝ : ℕ
⊢ v (n✝ + 1) ∈ s

Tactic:
· change w 0 ∈ s
      apply u_in

Goal state after:
case refine_2.succ
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n✝ : ℕ
⊢ v (n✝ + 1) ∈ s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case coe
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : ↑a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ ↑a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))

Tactic:
induction b with

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk a) = a

Tactic:
refine induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_
    rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range norm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : ⟨‖x‖, ⋯⟩ < ⟨‖y‖, ⋯⟩
⊢ ∃ a, ⟨‖x‖, ⋯⟩ < a ∧ a < ⟨‖y‖, ⋯⟩
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range nnnorm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : ⟨‖x‖₊, ⋯⟩ < ⟨‖y‖₊, ⋯⟩
⊢ ∃ a, ⟨‖x‖₊, ⋯⟩ < a ∧ a < ⟨‖y‖₊, ⋯⟩
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range nnnorm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
by
    rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
    let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
    exact ⟨⟨‖z‖₊, z, rfl⟩, h⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε

Tactic:
filter_upwards [hf δ δ₀, hC] with i hf hg

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
⊢ ‖op (f i) (g i)‖ < ε
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rwa [← ENNReal.coe_inj, ENNReal.coe_mul]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ⇑(e ^ n) = (⇑e)^[n]

Tactic:
← coe_toEquiv,

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ⇑(e ^ n).toEquiv = (⇑e)^[n]
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖↑n‖ * ‖x‖

Tactic:
by
  rw [← norm_smul, ← Int.smul_one_eq_cast, smul_assoc, one_smul]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k ↦ μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) ≤ ⨆ n, μ (s n)

Tactic:
set S := ⋃ n, s n

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
⊢ μ S ≤ ⨆ n, μ (s n)
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
i : ℕ
x : α
hx : x ∈ s i
⊢ ∃ i, x ∈ s i

Tactic:
exists i

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

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ I, b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
⊢ b < ∑' (i : α), f i

Tactic:
obtain ⟨I, hI⟩ := h b hb

Goal state after:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ I, b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
I : Finset α
hI : b < ∑ i ∈ I, f i
⊢ b < ∑' (i : α), f i
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
i : α
f g : α → ℝ≥0
h : ∀ (a : α), (fun i ↦ ↑(f i)) a ≤ (fun i ↦ ↑(g i)) a
hi : (fun i ↦ ↑(f i)) i < (fun i ↦ ↑(g i)) i
sf : ℝ≥0
hf : HasSum (fun i ↦ ↑(f i)) ↑sf
sg : ℝ≥0
hg : HasSum (fun i ↦ ↑(g i)) ↑sg
⊢ ↑sf < ↑sg

Tactic:
simp only [coe_le_coe, coe_lt_coe] at h hi ⊢

Goal state after:
case neg
α : Type u_1
i : α
f g : α → ℝ≥0
sf : ℝ≥0
hf : HasSum (fun i ↦ ↑(f i)) ↑sf
sg : ℝ≥0
hg : HasSum (fun i ↦ ↑(g i)) ↑sg
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
⊢ sf < sg
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
⊢ LowerSemicontinuous (s.indicator fun _x ↦ y)

Tactic:
by
  intro x z hz
  by_cases h : x ∈ s <;> simp [h] at hz
  · refine Filter.Eventually.of_forall fun x' => ?_
    by_cases h' : x' ∈ s <;> simp [h', hz, hz.trans_le hy]
  · filter_upwards [hs.isOpen_compl.mem_nhds h]
    simp +contextual [hz]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
⊢ ∀ (b' : ℕ), b' ≠ 0 → m (f b') = 0

Tactic:
rintro (_ | i)
        · simp
        · simp [f, m_empty]

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

Goal state before:

Tactic:
μ s + μ t ≤ (∑' i : I s, μ (f i)) + ∑' i : I t, μ (f i) :=
      add_le_add (hI _ subset_union_left) (hI _ subset_union_right)
    _ = ∑' i : ↑(I s ∪ I t), μ (f i) :=
      (ENNReal.summable.tsum_union_disjoint (f := fun i => μ (f i)) hd ENNReal.summable).symm
    _ ≤ ∑' i, μ (f i) :=
      (ENNReal.summable.tsum_le_tsum_of_inj (↑) Subtype.coe_injective (fun _ _ => zero_le)
        (fun _ => le_rfl) ENNReal.summable)
    _ ≤ ∑' i, m (f i) := ENNReal.tsum_le_tsum fun i => ofFunction_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.23
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0

Tactic:
simp [m_empty]

Goal state after:
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 : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ∑' (n : ℕ), m (f ⁻¹' (fun n ↦ (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
refine ENNReal.tsum_le_tsum fun n => le_of_eq ?_
    simp [hf.preimage_image]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0

Tactic:
simp [m_empty]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (restrict s) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun t ↦ m (t ∩ s)) ⋯

Tactic:
rw [restrict]
      simp only [inter_comm _ s, LinearMap.comp_apply]
      rw [comap_ofFunction _ (Or.inl hm)]
      simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
⊢ (c • m) ∅ = 0

Tactic:
simp [m_empty]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s

Tactic:
have : (fun s : Set α => ⨆ _ : s.Nonempty, m s) = m := by
    ext1 t
    rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]
  simp [boundedBy, this]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
by
  simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
  exact
    ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: 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 : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
h2 : a ∈ f ⟨b, h_b⟩
⊢ a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩

Tactic:
revert h2

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 : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ f ⟨b, h_b⟩ → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: 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 : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
h2 : a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩
⊢ a ∈ f ⟨b, h_b⟩

Tactic:
revert h2

Goal state after:
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 : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩
b : β
h_b : b ∈ s
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨b, h_b⟩ → a ∈ f ⟨b, h_b⟩
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
f g : α → β
⊢ f =ᵐ[μ] g ↔ μ {x | f x ≠ g x} = 0

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ s = ⇑e '' t ↔ ⇑e.symm '' s = t

Tactic:
← coe_toEquiv,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ s = ⇑e.toEquiv '' t ↔ ⇑e.symm '' s = t
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e '' ⇑e ⁻¹' s = s

Tactic:
← coe_toEquiv,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e.toEquiv '' ⇑e.toEquiv ⁻¹' s = s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ ⇑e ⁻¹' ⇑e '' s = s

Tactic:
← coe_toEquiv,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ ⇑e.toEquiv ⁻¹' ⇑e.toEquiv '' s = s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
π : δ' → Type u_6
inst✝ : (x : δ') → MeasurableSpace (π x)
f : δ ≃ δ'
⊢ ⇑(piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)

Tactic:
by rfl

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

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ⇑(sumPiEquivProdPi α) = ⇑(Equiv.sumPiEquivProdPi α)

Tactic:
by rfl

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

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ⇑(sumPiEquivProdPi α).symm = ⇑(Equiv.sumPiEquivProdPi α).symm

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ s = μ (t ∩ s) + μ (t \ s)

Tactic:
measure_inter_add_sdiff₀ _ hs,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ∞
⊢ μ s = μ t
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
⊢ NullMeasurable f μ ↔ EventuallyMeasurable m (ae μ) f

Tactic:
by rfl

Goal state after: