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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
⊢ x ∈ seqClosure s

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∈ s
⊢ x ∈ seqClosure s

case neg
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ seqClosure s = s

Tactic:
hs.seqClosure_eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ s = s
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
hb' : b' ≠ b
⊢ Pi.mulSingle b a b' = 1

Tactic:
simp [hb']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
⊢ ∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)

Tactic:
tprod_congr_set_coe _ Set.prod_singleton,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
⊢ ∏' (x : ↑((fun a ↦ (a, c)) '' s)), f ↑x = ∏' (b : ↑s), f (↑b, c)
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 (⋯.extend f (pkg.coe x)) (f x)

Tactic:
exact pkg.isDenseInducing.inseparable_extend hf.continuous.continuousAt

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : ↑f ≤ 𝓝 a
hb : ↑g ≤ 𝓝 b
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
rw [← tendsto_id'] at ha hb

Goal state after:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = ediam s

Tactic:
refine le_antisymm (ediam_le fun x hx y hy => ?_) (ediam_mono subset_closure)

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ edist x y ≤ ediam s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: s : Set ℝ
h : Bornology.IsBounded s
⊢ Metric.diam s = sSup s - sInf s

Tactic:
rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]

Goal state after:
s : Set ℝ
h : Bornology.IsBounded s
⊢ 0 ≤ sSup s - sInf s
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case neg
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 : ℕ
h : ∀ (n : ℕ), (x, y) ∈ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n

Tactic:
simp only [h, not_true, (pow_pos hr.1 _).not_ge]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ (limsup u f).toReal = b.truncateToReal (limsup u f)

Tactic:
rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|

Tactic:
rw [inf_comm c, inf_comm c]

Goal state after:
case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : FunLike F α✝ β
inst✝¹ : DilationClass F α✝ β
f : F
α : Type ?u.22
inst✝ : PseudoEMetricSpace α
x y : α
⊢ edist (id x) (id y) = ↑1 * edist x y

Tactic:
simp only [id, ENNReal.coe_one, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : Module R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : Module.IsTorsionFree R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ∞) = if c = 0 then 0 else ∞

Tactic:
simp_rw [smul_eq_zero, or_iff_left one_ne_zero]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
l : List α
hl : l ≠ []
⊢ (map norm l).prod = ↑(map nnnorm l).prod

Tactic:
simp [NNReal.coe_list_prod, List.map_map]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
l : List α
⊢ (map norm l).prod = ↑(map nnnorm l).prod

Tactic:
simp [NNReal.coe_list_prod, List.map_map]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
by
  rcases z.natAbs_eq with hz | hz
  · rw [← Int.cast_natCast, ← hz]
  · rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
⊢ ‖↑z.natAbs‖₊ = ‖↑z‖₊

Tactic:
by
  simp [← NNReal.coe_inj, -Nat.cast_natAbs, norm_natAbs]

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

Goal state before:
pp: case inl
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
⊢ ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i

Tactic:
rw [iSup_of_isEmpty, eq_comm, Finset.prod_eq_zero_iff]
    obtain ⟨a, ha⟩ := isEmpty_pi.mp h
    exact ⟨a, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = comap norm atTop⁻¹

Tactic:
← Filter.comap_inv

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = comap norm (comap Inv.inv atTop)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
s : ℝ
hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s
⊢ ∃ C, ∀ x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ, ‖x‖ ≤ C

Tactic:
exact ⟨s, fun x hx ↦ by simpa using hs (algebraMap 𝕜 𝕜' x) hx⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = f ⁻¹' {!true}

Tactic:
Bool.not_true

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = f ⁻¹' {false}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ y, ((fun x ↦ f (x, y)) ⁻¹' s) ×ˢ measurableAtom y

Tactic:
simp only [mem_preimage, mem_iUnion, mem_prod]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable fun x ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ f (x, y) ∈ s ↔ ∃ i, f (x, i) ∈ s ∧ y ∈ measurableAtom i
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ s ^ (2 * k + 1) = s

Tactic:
rw [zpow_add₀ hs, zpow_one, zpow_mul, zpow_two]

Goal state after:
case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ (s * s) ^ k * s = s
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
⊢ s ^ n = 1

Tactic:
by
  cases s <;> simp_all

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ ↑(sign x) * |x| = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ |x| * ↑(sign x) = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ ↑(sign x) * x = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
⊢ x * ↑(sign x) = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ∞
⊢ (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal

Tactic:
simp only [ENNReal.toReal, tsum_toNNReal_eq hf, NNReal.coe_tsum]

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

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ -↑|a|⁻¹ = (↑a)⁻¹

Tactic:
← coe_neg |a|⁻¹,

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(-|a|⁻¹) = (↑a)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i ↦ ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)

Tactic:
exact mod_cast NNReal.tendsto_sum_nat_add f

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

Goal state before:
pp: a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
cases a with
  | bot => simp
  | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

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

Goal state before:
pp: a : EReal
⊢ a ∈ Ioi 0 → ∀ ⦃b : EReal⦄, b ∈ Ioi 0 → a < b → (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a

Tactic:
a_0

Goal state after:
a : EReal
a_0 : a ∈ Ioi 0
⊢ ∀ ⦃b : EReal⦄, b ∈ Ioi 0 → a < b → (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a
Module: Mathlib.Data.EReal.Inv

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

Tactic:
false_or

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
Module: Mathlib.Data.EReal.Inv

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

Tactic:
false_or

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

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∉ s
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
⊢ Summable fun i ↦ if n ≤ i then 2⁻¹ ^ i else 0

Tactic:
simpa only [← piecewise_eq_indicator, one_div]
      using! summable_geometric_two.indicator {i | n ≤ i}

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

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

Tactic:
by
  simp only [div_eq_mul_inv, ENNReal.inv_pow] at hu
  refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu
  simp

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

Goal state before:
pp: case refine_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

Tactic:
refine le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_
    apply sInf_le hμ

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

Goal state before:
pp: a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ x < a / a * (2 * max (x + 1) 0 / 2)

Tactic:
mul_div_right_comm

Goal state after:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * max (x + 1) 0 / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * max (x + 1) 0 / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ x < a / a * (2 / 2 * max (x + 1) 0)
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:
simp [dissipate_def]

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:
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:
simp [dissipate_def]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
⊢ s 0 ⊆ dissipate s 0

Tactic:
simp [dissipate_def]

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

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

Tactic:
biUnion_lt_succ

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory ((⋃ k, ⋃ (_ : k < n), s k) ∪ s n)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
· exact continuousAt_mul_top_top

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k ↦ {s k}) S

Tactic:
refine ⟨{k}, fun m hm => ?_, s, fun i _ => ?_, ?_⟩

Goal state after:
case refine_2.refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S

case refine_2.refine_2
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k ↦ {s k}) i

case refine_2.refine_3
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ x ∈ {k}, s x
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ

Tactic:
convert! ae_eq_set_union (ae_eq_refl s) h

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ ↔ s ∪ t =ᵐ[μ] s ∪ univ
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] s

Tactic:
convert! ae_eq_set_union (ae_eq_refl s) h

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∪ t =ᵐ[μ] s ↔ s ∪ t =ᵐ[μ] s ∪ ∅
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
i : ι
⊢ μ (⋃ i_1 ∈ {i}ᶜ, s i ∩ s i_1) = 0

Tactic:
exact (measure_biUnion_null_iff <| to_countable _).2 fun j hj => hd (Ne.symm hj)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ Injective (map ⇑e)

Tactic:
intro μ₁

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ : Measure α
⊢ ∀ ⦃a₂ : Measure α⦄, map (⇑e) μ₁ = map (⇑e) a₂ → μ₁ = a₂
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos.mpr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ comap Subtype.val (𝓝[<] b) = atTop

Tactic:
refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_

Goal state after:
case pos.mpr.refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ ∀ i < b, ∃ i', True ∧ Ici i' ⊆ Subtype.val ⁻¹' Ioo i b

case pos.mpr.refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ ∀ (i' : { x // x ∈ s }), True → ∃ i < b, Subtype.val ⁻¹' Ioo i b ⊆ Ici i'
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) t
this : μ (⨆ i, s i) = ⨆ n, Function.extend e (fun x ↦ μ (s x)) (fun x ↦ 0) n
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
exact this.trans (iSup_extend_bot he _)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ := ⨆ D ∈ {D | D ⊆ C ∧ D.Countable}, μ (⋃₀ D)
hm : m = ⊥
⊢ μ (⋃₀ ∅) = m

Tactic:
simp [hm]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩

Goal state after:
case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx✝ : x ∈ s
U : Set α
hU : μ U < ∞
hx : x ∈ U
hUo : IsOpen[inst✝¹] U
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
δ : Type u_4
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
f g : α → δ
⊢ f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g

Tactic:
simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
⊢ 0 + 0 = 0

Tactic:
zero_add

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x

Tactic:
← map_comap_subtype_coe hs,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.map Subtype.val (Measure.comap Subtype.val μ), p x) ↔
    ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n)

Tactic:
refine measurableSet_generateFrom ?_
      rw [memPartition_succ]
      exact ⟨s, hs, by simp⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s ∩ t n)

Tactic:
refine measurableSet_generateFrom ?_
      rw [memPartition_succ]
      exact ⟨s, hs, by simp⟩

Goal state after: