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

Goal state before:
pp: case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun b ↦ f (2 * b + 1)

Tactic:
apply hf.comp_injective

Goal state after:
case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Injective fun b ↦ 2 * b + 1
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc y' x'

Tactic:
rwa [uIcc_comm]

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

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc y' x'

Tactic:
rwa [uIcc_comm]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)

Tactic:
rw [← summable_coe] at hf ⊢
  exact hf.comp_injective hi

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

Goal state before:
pp: case zero
ι : Sort u_1
n : ℕ
hn : 0 ≠ 0
⊢ (fun x ↦ x ^ 0) = ⇑(NNReal.powOrderIso 0 hn).withTopCongr

pp: case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr

Tactic:
(· cases hn rfl)

Goal state after:
case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
⊢ IsSeqCompact (f '' K)

Tactic:
by
  intro ys ys_in_fK
  choose xs xs_in_K fxs_eq_ys using ys_in_fK
  obtain ⟨a, a_in_K, phi, phi_mono, xs_phi_lim⟩ := K_cpt xs_in_K
  refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩
  exact (f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V
x : X
x✝ : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False

Tactic:
exact hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)

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

Goal state before:
pp: case refine_1.succ
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 : ℕ
hMl : M + 1 ≤ l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ d x (x :: l)[M + 1] ≤ L.sum

Tactic:
Nat.succ_le_iff

Goal state after:
case refine_1.succ
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 : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ d x (x :: l)[M + 1] ≤ L.sum
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ ∃ a,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖(j (a 0))⁻¹ * b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
exact
    ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀,
      fun n hn => by simpa [hg] using hv_pos n hn⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist (x, y).1 (x, y).2 ≤ edist (x', y').1 (x', y').2 + 2 * edist (x, y) (x', y')

Tactic:
calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by rw [edist_comm y y']; abel
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y

Tactic:
simp only [LipschitzOnWith, edist_nndist, dist_nndist]
  norm_cast

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

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

Tactic:
simpa only [NNReal.coe_one, one_mul]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
f : α → ℝ
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y
⊢ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul]

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

Goal state before:
pp: α : 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
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y

Tactic:
by
      rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x ↦ f x * g x) t

Tactic:
obtain ⟨Kf, t, ht, hKf⟩ := hf hx

Goal state after:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x ↦ f x * g x) t
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NormedRing α
inst✝ : NormMulClass α
a✝ b✝ : α
h : a✝ * b✝ = 0
⊢ a✝ = 0 ∨ b✝ = 0

Tactic:
by
    simpa only [← norm_eq_zero (E := α), norm_mul, mul_eq_zero] using h

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

Goal state before:
pp: case pos
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

pp: case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
· subst hji
      simp

Goal state after:
case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ Measurable f ↔ Measurable (f ∘ g)

Tactic:
by
  rw [measurable_iff_le_map, measurable_iff_le_map, ← map_comp, map_comap_eq_of_surjective hg]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}
⊢ MeasurableSet ({x | p x → q x} ∩ {x | q x → p x})

Tactic:
exact (hs.imp ht).inter (ht.imp hs)

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

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x y : β
hy : y ∉ measurableAtom x
⊢ ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s

Tactic:
simpa [measurableAtom] using hy

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

Goal state before:
pp: case ha
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ 0 < ‖(↑n)⁻¹‖

pp: case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖f (n • x)‖ < C

Tactic:
· simpa [pos_iff_ne_zero]

Goal state after:
case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖f (n • x)‖ < C
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ k ∈ range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ Summable fun k ↦ d (n + k)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ¬zero ≤ neg

Tactic:
by rintro ⟨_⟩

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

Goal state before:
pp: ⊢ ¬pos ≤ zero

Tactic:
by rintro ⟨_⟩

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

Goal state before:
pp: ⊢ ¬pos ≤ neg

Tactic:
by rintro ⟨_⟩

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by rintro ⟨_⟩

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

Tactic:
cases h₄ (h.trans_lt h₃)

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ ↑(comap f s.topologicalClosure) = closure[inst✝³] ↑(comap f s)

Tactic:
simp only [Subalgebra.coe_comap]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ ⇑f ⁻¹' ↑s.topologicalClosure = closure[inst✝³] (⇑f ⁻¹' ↑s)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
a : R
⊢ ∑' (i : α), a • f i = a • ∑' (i : α), f i

Tactic:
simpa only [smul_one_mul] using @ENNReal.tsum_mul_left _ (a • (1 : ℝ≥0∞)) _

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

Goal state before:
pp: case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (b * a)⁻¹ = b⁻¹ * a⁻¹

Tactic:
mul_comm b a,

Goal state after:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
a : ℝ
a_0 : 0 < ↑a
b_0 : 0 < ⊤
a_b : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹

Tactic:
| =>

Goal state after:
b : EReal
a : ℝ
a_0 : 0 < ↑a
b_0 : 0 < ⊤
a_b : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
a : ℝ
a_0 : 0 < ↑a
b_0 : 0 < ⊥
a_b : ↑a < ⊥
⊢ ⊥⁻¹ < (↑a)⁻¹

Tactic:
| =>

Goal state after:
b : EReal
a : ℝ
a_0 : 0 < ↑a
b_0 : 0 < ⊥
a_b : ↑a < ⊥
⊢ ⊥⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b✝ : EReal
a : ℝ
a_0 : 0 < ↑a
b : ℝ
b_0 : 0 < ↑b
a_b : ↑a < ↑b
⊢ (↑b)⁻¹ < (↑a)⁻¹

Tactic:
| =>

Goal state after:
b✝ : EReal
a : ℝ
a_0 : 0 < ↑a
b : ℝ
b_0 : 0 < ↑b
a_b : ↑a < ↑b
⊢ (↑b)⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < a ↔ b < a * c

Tactic:
nth_rw 1 [← @mul_div_cancel a c (ne_bot_of_gt h) h' h.ne']

Goal state after:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * (a / c) ↔ b < a * c
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
rw [range_coe_ennreal]

Goal state after:
⊢ (Ici 0).OrdConnected
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ IsClosed (range ENNReal.toEReal)

Tactic:
rw [range_coe_ennreal]

Goal state after:
⊢ IsClosed (Ici 0)
Module: Mathlib.Data.EReal.Inv

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

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

Tactic:
· rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁; exact h₁.rec

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

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

Tactic:
obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)
    exact ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt hc'⟩, (lt_div_iff b0 b_top.ne).1 hc'⟩

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y

Tactic:
obtain ⟨z₁, z₁lt, h₁⟩ : ∃ z₁ < f x, Ioc z₁ (f x) ⊆ u :=
      exists_Ioc_subset_of_mem_nhds (u_open.mem_nhds xu) hx₁

Goal state after:
case pos
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (fun z ↦ f z + g z) x1 > x2) x' y
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
a c : ℝ
ha : a ≠ 0
ha' : 0 < a
⊢ Tendsto (fun x ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atTop_zero.comp
      (tendsto_atTop_add_const_right _ c (tendsto_id.const_mul_atTop ha'))

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
⊢ (OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t ≤ ∑' (i : ℕ), m (f i)

Tactic:
set μ := OuterMeasure.ofFunction m m_empty

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this✝ : r ≠ 1
this : Tendsto (fun n ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)

Tactic:
simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
m : Set (OuterMeasure α)
s : Set α
hm : m.Nonempty
⊢ (restrict s) (sInf m) = sInf (⇑(restrict s) '' m)

Tactic:
simp only [sInf_eq_iInf, restrict_biInf, hm, iInf_image]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : s₂ ⊆ s₁
⊢ d.Has (s₁ \ s₂)

Tactic:
apply d.has_compl_iff.1
  simp only [sdiff_eq, compl_inter, compl_compl]
  exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s

Tactic:
h_eq,

Goal state after:
α : Type u_3
m : MeasurableSpace α
C : (s : Set α) → MeasurableSet s → Prop
s : Set (Set α)
h_eq : m = generateFrom s
h_inter : IsPiSystem s
empty : C ∅ ⋯
basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯
compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯
⊢ MeasurableSet = DynkinSystem.GenerateHas s
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
x : α
hx : ∀ (i : ι), aeSeq hf p i x = f i x
⊢ (⨆ n, aeSeq hf p n) x = (⨆ n, f n) x

Tactic:
simp [iSup_apply, hx]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (blimsup s atTop p)

Tactic:
by
  simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]
  exact .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim (sᶜ ∪ t') ≤ μ t'

Tactic:
rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self,
      Set.empty_union]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ μ (t' ∩ s) ≤ μ t'
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
⊢ c • μ ≪ c • ν

Tactic:
intro s hνs
  rw [smul_apply, ← smul_one_smul ℝ≥0∞, smul_eq_mul, mul_eq_zero] at hνs ⊢
  exact hνs.imp_right fun hs ↦ h hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
μ ν : Measure α
hf : MeasurableEmbedding f
hμν : μ ≪ ν
⊢ map f μ ≪ map f ν

Tactic:
by
  intro t ht
  rw [hf.map_apply] at ht ⊢
  exact hμν ht

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 = ∞
hμv : μ v ≠ ∞
⊢ False

Tactic:
apply hμuv

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 ≠ ∞
⊢ μ (u ∆ v) = ∞
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
rcases hs hsne with ⟨c, hcb, hcs⟩

Goal state after:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
⊢ (s ∩ Ioo a b).Nonempty
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (⇑μ + ⇑ν) univ < ∞

Tactic:
Pi.add_apply,

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ univ + ν univ < ∞