mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
⊢ H ≤ closure {a}

Tactic:
intro g

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
⊢ g ∈ H → g ∈ closure {a}
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (fun i ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) = fun s ↦ ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
ext s

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ ⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a = ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c d : EReal
h1 : c ≠ ⊥ ∨ d ≠ ⊤
h2 : c ≠ ⊤ ∨ d ≠ ⊥
⊢ a + b - (c + d) = a - c + (b - d)

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, sub_eq_add_neg, EReal.neg_add h1 h2, sub_eq_add_neg]
  grind

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c : β
hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a

Tactic:
exact hc.mono fun x hx => lt_of_lt_of_le hbc hx

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

Goal state before:
pp: case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -(↑x✝ * ⊥)

Tactic:
coe_mul_bot_of_pos h,

Goal state after:
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : 0 < x
⊢ x * (y + z) = x * y + x * z

Tactic:
lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩

Goal state after:
case inr
y z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (y + z) = ↑x * y + ↑x * z
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.hs
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), (s ↑j).Nonempty

Tactic:
push Not at H

Goal state after:
case neg.hs
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
H : ∀ (j : Subtype p), (s ↑j).Nonempty
⊢ ∀ (j : Subtype p), (s ↑j).Nonempty
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ HasProd f (finprod (L.support.mulIndicator fun b ↦ f b)) L

pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L

Tactic:
· convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : HasProd (fun b ↦ f b) 1 L
⊢ HasProd f 1 L

case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : ¬(L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite)
h' : ¬HasProd (fun b ↦ f b) 1 L
⊢ HasProd f (Exists.choose ha) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

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

Tactic:
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

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

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf : Function.Even f
hf2 : Multipliable f
⊢ ∏' (n : ℤ), f n = f 0 * (∏' (n : ℕ+), f ↑↑n) ^ 2

Tactic:
by
  simpa only [sq, ← mul_assoc, hf _] using tprod_int_eq_zero_mul_tprod_pnat hf2

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

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ y' - x'

Tactic:
by
  simpa only [Real.dist_eq, abs_of_nonpos (sub_nonpos.2 <| hx.1.trans hx.2), neg_sub] using
    Real.dist_le_of_mem_uIcc (Icc_subset_uIcc hx) (Icc_subset_uIcc hy)

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

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a ↦ ↑(f (a + k))) ↔ Summable fun a ↦ ↑(f a)

Tactic:
exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)

Tactic:
rw [mul_comm, ← div_eq_mul_inv]
  exact ENNReal.div_le_of_le_mul' (hf x y)

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

Goal state before:
pp: case e'_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ (fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm =
    (fun p ↦ p.1 * p.2) ∘ Prod.map (fun s ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun s ↦ ∏ b ∈ s, (f ∘ Sum.inr) b

Tactic:
ext s

Goal state after:
case e'_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
s : Finset α × Finset β
⊢ ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) s =
    ((fun p ↦ p.1 * p.2) ∘ Prod.map (fun s ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun s ↦ ∏ b ∈ s, (f ∘ Sum.inr) b) s
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
⊢ comap norm (𝓝 0) = 𝓝 1

Tactic:
by
  simpa only [dist_one_right] using nhds_comap_dist (1 : E)

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
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
m : ℕ
hm : List.IsChain (fun x y ↦ d x y = 0) (x :: l ++ [y])
hLm : L.length ≤ m
⊢ False

Tactic:
exact hd₀ (hm.rel_cons (mem_append.2 <| Or.inr <| mem_singleton_self _))

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

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (pkg.extend f (pkg.coe x)) (f x)

Tactic:
by
  rw [extend_def _ hf]
  exact pkg.isDenseInducing.inseparable_extend hf.continuous.continuousAt

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

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

Tactic:
simp only [Finset.prod_insert has]

Goal state after:
case insert
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ Tendsto (fun b ↦ f a✝ b * ∏ c ∈ s✝, f c b) x (𝓝 (a a✝ * ∏ c ∈ s✝, a c))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ⊢ ContinuousOn (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)}

Tactic:
ContinuousOn

Goal state after:
⊢ ∀ x ∈ {p | p ≠ (∞, ∞)}, ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous fun x ↦ a - x

Tactic:
by
  change Continuous (Function.uncurry Sub.sub ∘ (a, ·))
  refine continuousOn_sub.comp_continuous (.prodMk_right a) fun x => ?_
  simp only [a_ne_top, Ne, mem_ofPred_eq, Prod.mk_inj, false_and, not_false_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : ↑δ * C < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)

Tactic:
rw [mul_comm] at hδ

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ Continuous t.truncateToReal

Tactic:
apply continuousOn_toReal.comp_continuous (by fun_prop)
  simp [t_ne_top]

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

Goal state before:
pp: ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun i ↦ f i - c) F = limsup f F - c

Tactic:
by
  rcases F.eq_or_neBot with rfl | _
  · simp
  · exact (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzAdd.C ℝ) fun p ↦ p.1 + p.2

Tactic:
by
    rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
    exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
q : α × α
this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
⊢ Filter.Tendsto (fun t ↦ ‖t.1 - q.1‖ + ‖t.2 - q.2‖) (nhds q) (nhds 0)

Tactic:
convert!
    ((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
      ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm

Goal state after:
case e'_5
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
q : α × α
this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
⊢ 0 = ‖q.1 - q.1‖ + ‖q.2 - q.2‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (b * a) a = ‖b‖

Tactic:
by
  rw [dist_comm, dist_mul_self_right]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖

Tactic:
exact norm_sub_mul_le (α := αᵐᵒᵖ) hb

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖

Tactic:
rw [add_comm]; exact norm_sub_mul_le (α := αᵐᵒᵖ) hb

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

Goal state before:
pp: x : ℝ≥0
⊢ ‖↑x‖ = ↑x

Tactic:
by rw [Real.norm_eq_abs, x.abs_eq]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.2 hj = TProd.elim w.2 hj

Tactic:
rw [← elim_of_mem hl, hvw, elim_of_mem hl]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Subsingleton α
⊢ MeasurableSingletonClass α

Tactic:
refine ⟨fun i => ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Subsingleton α
i : α
⊢ MeasurableSet {i}
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

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

Tactic:
rcases exists_surjective_nat ι with ⟨e, he⟩

Goal state after:
case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ b, f b)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
⊢ ⨆ n, m n = generateFrom {s | ∃ n, MeasurableSet s}

Tactic:
ext s

Goal state after:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
S : Set (Set α)
hS : S.Countable
⊢ μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0

Tactic:
rw [sUnion_eq_biUnion, measure_biUnion_null_iff hS]

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

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

Tactic:
rw [ENNReal.tsum_comm]

Goal state after:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ ∑' (i : ι), (f i) (⋃ i, s i) ≤ ∑' (b : ι) (a : ℕ), (f b) (s a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤
    MeasurableSpace.comap (fun b c ↦ g c b) (MeasurableSpace.comap (fun b ↦ b a) (inst✝ a))

Tactic:
by measurability

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

Goal state before:
pp: ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst✝ : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
x✝ : Sigma κ
⊢ Measurable fun c ↦ Sigma.uncurry c x✝

Tactic:
simp only [Sigma.uncurry]

Goal state after:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst✝ : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
x✝ : Sigma κ
⊢ Measurable fun c ↦ c x✝.fst x✝.snd
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

Tactic:
neg_eq_neg_one,

Goal state after:
case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = -1
⊢ sign (∑ i ∈ s, f i) = -1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Zero α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Zero β
inst✝³ : Preorder β
inst✝² : DecidableLT β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ sign (f a) = sign a

Tactic:
by
  simp only [sign_apply, ← map_zero f, hf.lt_iff_lt]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
rcases trichotomy (sign a) with hsa | hsa | hsa <;>
    rcases trichotomy (sign b) with hsb | hsb | hsb <;>
    simp_all

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

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

Tactic:
ENNReal.hasSum_iff_tendsto_nat

Goal state after:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case bot
⊢ 0 = -⊥⁻¹

Tactic:
inv_bot,

Goal state after:
case bot
⊢ 0 = -0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ ⊥⁻¹ = -⊤⁻¹

Tactic:
inv_bot,

Goal state after:
case top
⊢ 0 = -⊤⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
⊢ Summable f

Tactic:
refine summable_iff_not_tendsto_nat_atTop.2 fun H => ?_
  rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
  exact lt_irrefl _ (hn.trans_le (h n))

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

Goal state before:
pp: case top_pos
x : ℝ
x_pos : 0 < x
⊢ (⊤ * ↑x)⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
top_mul_of_pos (EReal.coe_pos.2 x_pos),

Goal state after:
case top_pos
x : ℝ
x_pos : 0 < x
⊢ ⊤⁻¹ = ⊤⁻¹ * (↑x)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_neg
x : ℝ
x_neg : x < 0
⊢ ⊥⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
inv_bot,

Goal state after:
case top_neg
x : ℝ
x_neg : x < 0
⊢ 0 = ⊤⁻¹ * (↑x)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case pos_bot
x : ℝ
x_pos : 0 < x
⊢ ⊥⁻¹ = (↑x)⁻¹ * ⊥⁻¹

Tactic:
inv_bot,

Goal state after:
case pos_bot
x : ℝ
x_pos : 0 < x
⊢ 0 = (↑x)⁻¹ * 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_bot
x : ℝ
x_neg : x < 0
⊢ 0 = (↑x)⁻¹ * ⊥⁻¹

Tactic:
inv_bot,

Goal state after:
case neg_bot
x : ℝ
x_neg : x < 0
⊢ 0 = (↑x)⁻¹ * 0
Module: Mathlib.Topology.Semicontinuity.Defs

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

Tactic:
upperHemicontinuousOn_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
s : Set α
⊢ (∀ x ∈ s, UpperHemicontinuousWithinAt f s x) ↔
    ∀ x ∈ s, ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow (f '' s)

Tactic:
| inl h =>

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

Goal state before:
pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
· have b0 : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
    obtain ⟨a', ha', aa'⟩ := exists_between ((div_lt_iff b0 b_top).2 h)
    exact ⟨a', ⟨(div_nonneg hc b0.le).trans_lt ha', aa'⟩, (div_lt_iff b0 b_top).1 ha'⟩

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

Goal state before:
pp: ⊢ (range Real.toEReal).OrdConnected

Tactic:
by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

Tactic:
by
  ext1 s
  have : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩
  simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
  iInf_subtype']
  rw [ENNReal.mul_iInf fun h => (hc h).elim]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ dissipate s x ↔ ∀ y ≤ x, z ∈ s y

Tactic:
by
  simp [dissipate_def]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
inst✝ : Preorder α
s : α → Set β
x : α
⊢ ⋂ y, ⋂ (_ : y ≤ x), dissipate s y ⊆ dissipate s x

Tactic:
apply iInter_mono fun z y hy ↦ ?_
    simp only [mem_iInter, mem_dissipate] at *
    exact fun h ↦ hy h z le_rfl

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : α → Set β
⊢ dissipate s ⊥ = s ⊥

Tactic:
by
  simp [dissipate_def]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
⊢ dissipate s 0 = s 0

Tactic:
by
  simp [dissipate_def]

Goal state after: