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

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
x : ℤ
hx : x ∈ u
h'x : x ≤ 0
⊢ (∃ a ∈ v', ↑a = x) ∨ ∃ a ∈ v', -↑a = x

Tactic:
· refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [abs_of_nonpos h'x, Int.natCast_natAbs, neg_neg]

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
⊢ ∏' (i : ι), f i ∈ s

Tactic:
by_cases hf : Multipliable f

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : Multipliable f
⊢ ∏' (i : ι), f i ∈ s

case neg
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ dist x' y'

Tactic:
by
  refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b) <;> refine Icc_subset_uIcc ?_
  exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]

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

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
n : ℕ
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
lift f to ι → ℝ≥0 using hf; dsimp; exact mod_cast NNReal.iSup_pow f n

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

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

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

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
X : α → Type u_5
inst✝¹ : (x : α) → CommMonoid (X x)
inst✝ : (x : α) → TopologicalSpace (X x)
L : SummationFilter ι
f : ι → (x : α) → X x
⊢ Multipliable f L ↔ ∀ (x : α), Multipliable (fun i ↦ f i x) L

Tactic:
simp only [Multipliable, Pi.hasProd, Classical.skolem]

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
⊢ False

Tactic:
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)

Goal state after:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun n ↦ ↑(Real.nnabs (x n))) l, ↑r ≤ n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
⊢ False

Tactic:
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)

Goal state after:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun n ↦ ↑(Real.nnabs (x n))) l, ↑r ≤ n
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_7
inst✝ : NormedCommGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
simp_rw [← norm_inv_mul]

Goal state after:
E : Type u_7
inst✝ : NormedCommGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y
⊢ ∀ (x y : α), dist (f x) (f y) ≤ ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul] using h

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y
⊢ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul] using h

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

Goal state before:
pp: case refine_2
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 : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
⊢ ∀ (i' : ℕ), True → ∃ i, True ∧ {p | dist p.1 p.2 < ↑(1 / 2) ^ i} ⊆ U i'

Tactic:
refine fun n _ => ⟨n + 1, trivial, fun x hx => ?_⟩

Goal state after:
case refine_2
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 : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∈ {p | dist p.1 p.2 < ↑(1 / 2) ^ (n + 1)}
⊢ x ∈ U n
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ ‖u 0‖ + C

Tactic:
refine (norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u 0‖ + ‖(u n)⁻¹ * u 0‖ ≤ ‖u 0‖ + C
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α✝ : Type u_2
β : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ ‖1‖ = 1

Tactic:
by simpa [Pi.norm_def] using Finset.sup_const Finset.univ_nonempty 1

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

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

Tactic:
Classical.nonempty_pi

Goal state after:
case inr.refine_2
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty (ι i)
⊢ ∏ a, ⨆ i, f a i ≤ ⨆ i, ∏ a, f a (i a)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
hm : n < 0
hc : ContinuousAt (fun x ↦ x ^ n) 0
⊢ False

Tactic:
exact (hc.tendsto.mono_left nhdsWithin_le_nhds).not_tendsto (Metric.disjoint_nhds_cobounded _)
    (tendsto_zpow_nhdsNE_zero_cobounded hm)

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

Goal state before:
pp: case mpr.inl
K : Type u_4
inst✝ : NormedField K
h : IsComplete (closedBall 0 1)
h✝ : DiscreteTopology K
⊢ IsComplete Set.univ

Tactic:
← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete

Goal state after:
case mpr.inl
K : Type u_4
inst✝ : NormedField K
h : IsComplete (closedBall 0 1)
h✝ : DiscreteTopology K
⊢ IsComplete (closedBall 0 1)
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:
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: 𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁷ : NormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E✝
inst✝³ : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ ‖a • f‖ ≤ ‖a‖ * ‖f‖

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def,
      NNReal.mul_finset_sup]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁷ : NormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E✝
inst✝³ : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ (Finset.univ.sup fun b ↦ ‖(a • f) b‖₊) ≤ Finset.univ.sup fun a_1 ↦ ‖a‖₊ * ‖f a_1‖₊
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable f ↔ ¬Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
← not_iff_not,

Goal state after:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ ¬¬Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
← not_iff_not,

Goal state after:
f : ℕ → ℝ≥0
⊢ ¬Summable f ↔ ¬¬Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
⊢ IsOpen[inst✝¹] {x' | b ∈ f x'}

Tactic:
simpa using h.preimage (continuous_id.prodMk continuous_const)

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

Goal state before:
pp: a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd✝¹ : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd✝ : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
b' : EReal
bb' : b' ∈ Ioo b ⊤
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le

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

Goal state before:
pp: ⊢ Tendsto toReal (𝓝[≠] ⊤) atTop

Tactic:
nhdsWithin_top,

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
rw [h, bot_add]

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ (OuterMeasure.ofFunction m m_empty) s = ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)

Tactic:
OuterMeasure.ofFunction_apply

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (t n) =
    ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ↑a)

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]

Goal state after:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ↑a), a.1 + a.2 < ↑x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ⊥)

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]

Goal state after:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < ↑x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)

Tactic:
by
  rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
  rw [← ENNReal.coe_zero]
  norm_cast at *
  apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }

Tactic:
have hf : HasSum f ε := hasSum_geometric_two' _

Goal state after:
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.11
inst✝ : Encodable ι
f : ℕ → ℝ := fun n ↦ ε / 2 / 2 ^ n
hf : HasSum f ε
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

Tactic:
by_cases h : P s

Goal state after:
case pos
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

case neg
R : Type u_1
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

Tactic:
by_cases h : P s

Goal state after:
case pos
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s

case neg
α : Type u_2
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
s : α
h : ¬P s
⊢ (c • extend m) s = extend (fun s h ↦ c • m s h) s
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂

Tactic:
by
  refine le_iInf ?_
  intro h₂
  rw [extend_eq m h₁]
  exact m_mono h₁ h₂ hs

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
⊢ d.Has (tᶜ ∩ s)

Tactic:
have : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ := Set.ext fun x => by by_cases h : x ∈ s <;> simp [h]
    simp_rw [this]
    exact
      d.has_sdiff (d.has_compl hts) (d.has_compl h)
        (compl_subset_compl.mpr inter_subset_right)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ae μ ≤ ae ν
s : Set α
⊢ (∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s

Tactic:
exact fun hs => h hs

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
hμuv : μ (u ∆ v) ≠ ∞
hμu : μ u = ∞
⊢ μ v = ∞

Tactic:
by_contra! hμv

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : μ (s ∆ t) ≠ ∞
u v : Set α
hμuv : μ (u ∆ v) ≠ ∞
hμu : μ u = ∞
hμv : μ v ≠ ∞
⊢ False
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → ↑(Ioo a b)
ha : IsPredPrelimit a
⊢ Tendsto f l atBot ↔ Tendsto (fun x ↦ ↑(f x)) l (𝓝[>] a)

Tactic:
by
  rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ μ (⋂ i, f i) = μ (⋂ i, ⋂ j, ⋂ (_ : j ≤ i), f j)

Tactic:
rw [iInter_comm]

Goal state after:
α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ μ (⋂ i, f i) = μ (⋂ i', ⋂ i, ⋂ (_ : i' ≤ i), f i')
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite

Tactic:
← Set.finite_coe_iff

Goal state after:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑{s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_1.compl.refine_2.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ Codisjoint (⋃₀ (memPartition t n \ ↑S)) (⋃₀ ↑S)

Tactic:
· rw [codisjoint_iff]
          simp only [sup_eq_union, top_eq_univ]
          rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_sdiff_cancel hS_subset]

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

Goal state before:
pp: case refine_1.succ.inr
α : Type u_1
t : ℕ → Set α
n : ℕ
ih : ∀ u ∈ memPartition t n, MeasurableSet u
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v \ t n)

Tactic:
· exact (ih v hv).diff (measurableSet_generateFrom ⟨n, rfl⟩)

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
s : Set α
hs : NullMeasurableSet s (sum f)
⊢ (sum f) s = ∑' (i : ι), (f i) s

Tactic:
by
  apply le_antisymm ?_ (le_sum_apply _ _)
  rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, t_meas, ht⟩
  calc
  sum f s = sum f t := measure_congr ht.symm
  _ = ∑' i, f i t := sum_apply _ t_meas
  _ ≤ ∑' i, f i s := ENNReal.tsum_le_tsum fun i ↦ measure_mono ts

Goal state after:
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hK : IsClosed[inst✝²] K
hyK : y ∈ K
⊢ x ∈ K

Tactic:
apply IsClosed.isGδ at hK

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hyK : y ∈ K
hK : IsGδ K
⊢ x ∈ K
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: γ : Type u_3
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ μ (closure[inst✝³] K) ≤ μ K

Tactic:
calc
    μ (closure K) ≤ μ (toMeasurable μ K) := measure_mono <|
      hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
    _ = μ K := measure_toMeasurable ..

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Iio)

Tactic:
refine le_antisymm ?_ (generateFrom_le ?_)

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α ≤ MeasurableSpace.generateFrom (range Iio)

case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ t ∈ range Iio, MeasurableSet t