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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, a < b
⊢ liminf f (𝓝[>] a) = ⨆ r, ⨆ (_ : r > a), f r

Tactic:
rw [(nhdsGT_basis_of_exists_gt hb).liminf_eq_iSup_iInf]

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, a < b
⊢ ⨆ i, ⨆ (_ : a < i), ⨅ a_1 ∈ Set.Ioo a i, f a_1 = ⨆ r, ⨆ (_ : r > a), f r
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L

Tactic:
simp_rw [HasProd, comp_apply, ← _root_.map_prod]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ Tendsto (fun s ↦ g (∏ x ∈ s, f x)) L.filter (𝓝 (g a)) ↔ Tendsto (fun s ↦ ∏ x ∈ s, f x) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) g ↔ HasProd (fun x ↦ f ↑x) g

Tactic:
rw [← (notMemRangeEquiv k).symm.hasProd_iff, Function.comp_def, coe_notMemRangeEquiv_symm]

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
f : α → G
inst✝¹ : FirstCountableTopology G
inst✝ : T1Space G
hf : Multipliable f
⊢ (mulSupport f).Countable

Tactic:
simpa only [ker_nhds] using! hf.tendsto_cofinite_one.countable_compl_preimage_ker

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L

Tactic:
simp_rw [HasProd, Finset.prod_inv_distrib]

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ Tendsto (fun s ↦ (∏ x ∈ s, f x)⁻¹) L.filter (𝓝 a⁻¹)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(g '' mulSupport (f ∘ g)).Finite
⊢ ¬(mulSupport (f ∘ g)).Finite

Tactic:
Set.finite_image_iff hg.injOn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport (f ∘ g)).Finite
⊢ ¬(mulSupport (f ∘ g)).Finite
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
⊢ (∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h

Tactic:
by_cases hP : P <;> simp [hP]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → P → α
⊢ (∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1

Tactic:
by_cases hP : P <;> simp [hP]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ Multipliable (fun x ↦ 0) L

Tactic:
by
  obtain hβ | hβ := isEmpty_or_nonempty β
  · simp
  · exact ⟨0, hasProd_zero_zero⟩

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

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

Tactic:
NNReal.coe_zero

Goal state after:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun a ↦ ∑' (a_1 : { x // x ∉ a }), ↑(f ↑a_1)) atTop (𝓝 0)
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 : X
⊢ (zipWith d [x] ([] ++ [x])).sum = 0

Tactic:
simp [dist_self]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
by
  have := hl.1
  rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
  choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
  have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx =>
    @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
  obtain ⟨t, ht_anti, htl, htW, hts⟩ :
      ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s := by
    have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
      rw [le_principal_iff] at hls
      have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
      simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using! this
    choose t htl htW hts using this
    have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
    exact ⟨fun n => ⋂ k ≤ n, t k, fun m n h =>
      biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n =>
      (prod_mono (this n) (this n)).trans (htW n), fun n => (this n).trans (hts n)⟩
  choose u hu using fun n => Filter.nonempty_of_mem (htl n)
  have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
      ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
  rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩
  refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
  obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=
    ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists
  refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
  exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩

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

Goal state before:
pp: case refine_1.zero
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
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
hMl : 0 ≤ l.length
hMs : IsGreatest s 0
hM_lt : 0 < L.length
hM_ltx : 0 < (x :: l).length
hM_lty : 0 < (l ++ [y]).length
⊢ d x (x :: l)[0] ≤ L.sum

Tactic:
simp [dist_self]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
⊢ s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s

Tactic:
by
  refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))
  exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun b ↦ a / m b) f (𝓝 (a / b))

Tactic:
by
  apply Tendsto.const_mul (tendsto_inv_iff.2 hm)
  simp [hb]

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

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

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

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ LipschitzWith K (hs.extend f)

Tactic:
by
  have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
    apply isClosed_le (by fun_prop)
    exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop)
  have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    apply (hs.prod hs).mono
    rintro ⟨x, y⟩ ⟨hx, hy⟩
    have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
    have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩
    simp only [Set.mem_ofPred_eq, Ax, Ay]
    exact hf ⟨x, hx⟩ ⟨y, hy⟩
  simpa only [Dense, IsClosed.closure_eq, Set.mem_ofPred_eq, Prod.forall] using! this

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ g x - ↑K * dist x y ≤ f ↑z + ↑K * dist y ↑z

Tactic:
sub_le_iff_le_add

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ g x ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case neg
ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
h : 0 ≠ a
⊢ s.sup' hs f * a = s.sup' hs fun i ↦ f i * a

Tactic:
exact map_finset_sup' (OrderIso.mulRight₀ _ (lt_of_le_of_ne ha h)) hs f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)

Tactic:
have hr : ratio f ≠ 0 := ratio_ne_zero f

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ f y ∈ eball (f x) (↑(ratio f) * r)

Tactic:
rw [Metric.mem_eball, edist_eq f y x]

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) * edist y x < ↑(ratio f) * r
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ b, f b)

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simp
  · rcases exists_surjective_nat ι with ⟨e, he⟩
    rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]
    exact m.measurableSet_iUnion _ fun _ => h _

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

Goal state before:
pp: case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0

Tactic:
sub_ne_zero,

Goal state after:
case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k ≠ (Infinite.natEmbedding 𝕜) n
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)

Tactic:
exact Nat.cast_pos.2 (Nat.succ_pos _)

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]
  split_ifs with h h'
  · exact False.elim (lt_asymm h h')
  · simp
  · simp
  · simp

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

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

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
  convert! ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)
  rw [ENNReal.coe_tsum]
  exact NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective

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

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

Tactic:
rintro (h | h | h | h)
    · exact (sign.monotone.reflect_lt h).le
    all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]

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

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

Tactic:
rintro hnat ⟨r, hr⟩

Goal state after:
case mpr
f : ℕ → ℝ≥0
hnat : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
exact NNReal.coe_lt_coe.1 this

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

Goal state before:
pp: case bot
⊢ ⊥⁻¹ < ⊤

Tactic:
exact inv_bot ▸ zero_lt_top

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

Goal state before:
pp: a b c : EReal
⊢ a * (b / c) = b * (a / c)

Tactic:
rw [mul_div a b c, mul_comm a b, ← mul_div b a c]

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

Goal state before:
pp: a b c : EReal
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹

Tactic:
rw [mul_assoc a b⁻¹, mul_inv]

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

Goal state before:
pp: a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ Tendsto toReal (𝓝 a) (𝓝 a.toReal)

Tactic:
lift a to ℝ using ⟨ha, h'a⟩

Goal state after:
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto toReal (𝓝 ↑a) (𝓝 (↑a).toReal)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inl
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
obtain ⟨a', aa', a_top'⟩ := exists_between a_top

Goal state after:
case inr.inl
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
a' : EReal
aa' : a < a'
a_top' : a' < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Iic y)

Tactic:
rw [lowerSemicontinuous_iff_isOpen_preimage]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst✝¹] (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Iic y)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ 𝓝[≠] ⊤ = map Real.toEReal atTop

Tactic:
by
  apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
  · simp only [EReal.image_coe_Ici, true_and]
    intro x hx
    by_cases hx_bot : x = ⊥
    · simp [hx_bot]
    lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h1, h2.ne_top]
  · simp only [EReal.image_coe_Ici, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ⊤) ↔ Tendsto f l atTop

Tactic:
rw [tendsto_nhds_top_iff_real, atTop_basis_Ioi.tendsto_right_iff]; simp

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

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
refine mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_

Goal state after:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∃ᶠ (a : α) in f, c < (u * v) a
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (a * (↑h)⁻¹ + c) / (b * (↑h)⁻¹ + d) = (a + c * ↑h) / (b + d * ↑h)

Tactic:
field (discharger := norm_cast)

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

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

Tactic:
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.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f

Tactic:
refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_
  rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
  finiteness [(tsub_pos_iff_lt.2 hr).ne']

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:
restrict

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val ∘ₗ comap Subtype.val) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t ↦ m (t ∩ s)) ⋯
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s

Tactic:
le_boundedBy,

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ (∀ (s : Set α), μ s ≤ m s) ↔ ∀ (s : Set α), s.Nonempty → μ s ≤ m s
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

Tactic:
simp only [boundedBy, smul_ofFunction hc]
  congr 1 with s : 1
  rcases s.eq_empty_or_nonempty with (rfl | hs) <;> simp [*]

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ ⨆ i, m (t ∩ ⋃ i_1, ⋃ (_ : i_1 < i), s i_1) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
refine iSup_le fun n => ?_

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
n : ℕ
⊢ m (t ∩ ⋃ i, ⋃ (_ : i < n), s i) + m (t \ ⋃ i, s i) ≤ m t
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
⊢ ⨆ i, ∑ a ∈ Finset.range i, m (s a) ≤ m (⋃ i, s i)

Tactic:
refine iSup_le fun n => ?_

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ a ∈ Finset.range n, m (s a) ≤ m (⋃ i, s i)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ piiUnionInter (fun i ↦ {s i}) S = {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}

Tactic:
by
  ext1 s'
  simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_ofPred_eq]
  refine ⟨fun h => ?_, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩
  grind

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace ((generate s).toMeasurableSpace ⋯) ≤ ofMeasurableSpace (generateFrom s)

Tactic:
ofMeasurableSpace_toMeasurableSpace

Goal state after:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ (toMeasurable μ s) = μ s

Tactic:
rw [toMeasurable_def]; split_ifs with hs h's
  · exact measure_congr hs.choose_spec.2.2
  · simpa only [inter_univ] using h's.choose_spec.2.2 univ MeasurableSet.univ
  · exact (exists_measurable_superset μ s).choose_spec.2.2

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝¹ : SupSet β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f n x
⊢ ⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n

Tactic:
filter_upwards [aeSeq_eq_fun_ae hf hp] with x hx
  simp [iSup_apply, hx]

Goal state after: