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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
⊢ IsCompact (closedBall x₀ r)

Tactic:
have B : IsBounded K := hK.isBounded_preimage isBounded_closedBall

Goal state after:
β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
⊢ IsCompact (closedBall x₀ r)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.sphere x r = Metric.sphere (h x) r

Tactic:
by
  rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
⊢ TotallyBounded s

Tactic:
intro V

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
V : Set (X × X)
⊢ V ∈ 𝓤 X → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (x - ε) (x + ε)

Tactic:
refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
    · rintro ⟨a, b⟩ ⟨ha, hb⟩
      rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
      rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
      refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
      · exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)
      · grw [min_le_right]
        exact hδ
    · exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
        lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
n : ℕ
⊢ {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E

Tactic:
simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)

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

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

pp: case neg
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

Tactic:
· rw [pkg.extend_def hf]
    exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf

Goal state after:
case neg
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (pkg.extend f)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑x < y.1 - y.2

Tactic:
lt_tsub_iff_left,

Goal state after:
b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ y.2 + ↑x < y.1
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f

Tactic:
delta gen

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' fun s ↦ {p | s ∈ ↑p.1 ×ˢ ↑p.2}) = (𝓤 α).lift' f
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:
| insert _ _ has IH =>

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

Goal state before:
pp: case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ Metric.diam s

Tactic:
← Metric.diam_closure

Goal state after:
case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ Metric.diam (closure s)
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case pos
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
⊢ Nat.find h ≤ n ↔ (x, y) ∉ U n

Tactic:
Nat.find_le_iff

Goal state after:
case pos
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
⊢ (∃ m ≤ n, (x, y) ∉ U m) ↔ (x, y) ∉ U n
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ liminf (f + g) u = liminf f u

Tactic:
by
  refine le_antisymm ?_ <| liminf_le_liminf <| .of_forall <| by simp
  refine liminf_le_of_le (by isBoundedDefault) fun b hb ↦ ?_
  rw [Filter.le_liminf_iff']
  rintro a hab
  filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| lt_min (tsub_pos_of_lt hab) one_pos]
    with i hfg hg
  exact ENNReal.le_of_add_le_add_right (hg.trans_lt <| by simp).ne <|
    (add_le_of_le_tsub_left_of_le hab.le <| hg.trans <| min_le_left ..).trans hfg

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto f l (comap norm atTop)

Tactic:
tendsto_comap_iff

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop
Module: Mathlib.Topology.MetricSpace.Dilation

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

Tactic:
edist_nndist,

Goal state after:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ ↑(nndist x y) ≠ 0
Module: Mathlib.Topology.MetricSpace.Dilation

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

Tactic:
edist_nndist,

Goal state after:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ ↑(nndist (f x) (f y)) = ↑r * edist x y
Module: Mathlib.Topology.MetricSpace.Dilation

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

Tactic:
edist_nndist,

Goal state after:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ ↑(nndist (f x) (f y)) = ↑r * ↑(nndist x y)
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✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ edist (f x) (f y) = ↑r * edist x y

Tactic:
edist_nndist,

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑r * edist x y
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✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑r * edist x y

Tactic:
edist_nndist,

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑r * ↑(nndist x y)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
q : ℚ
h : r₁ < ↑q ∧ ↑q < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂

Tactic:
rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ b, bif b then s₁ else s₂)

Tactic:
exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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

Goal state before:
pp: case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
⊢ z ∈ ⋂ y ∈ (measurableAtom x)ᶜ, s y

Tactic:
simp only [mem_iInter, mem_compl_iff]

Goal state after:
case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
z : β
hz : z ∈ measurableAtom x
⊢ ∀ i ∉ measurableAtom x, z ∈ s i
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)
⊢ Measurable Sigma.uncurry

Tactic:
refine measurable_pi_lambda _ fun _ ↦ ?_

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 ↦ Sigma.uncurry c x✝
Module: Mathlib.Data.Nat.Cast.Order.Field

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

pp: case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1

Tactic:
· exact Nat.cast_add_one_pos _

Goal state after:
case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ ↑n + 1 ≤ ↑m + 1
Module: Mathlib.Data.Nat.Cast.Order.Field

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

pp: case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1

Tactic:
· exact Nat.cast_add_one_pos _

Goal state after:
case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ ↑n + 1 < ↑m + 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
⊢ a / 0 = 0

Tactic:
by
  change a * 0⁻¹ = 0
  rw [inv_zero, mul_zero a]

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

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

Tactic:
mul_div a b c,

Goal state after:
a b c : EReal
⊢ a * b / c = b * (a / c)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ c = a * b

pp: case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a

Tactic:
· rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]

Goal state after:
case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
    tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ (fun i ↦ extend m (s i)) = fun i ↦ m (s i) ⋯

Tactic:
funext i

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
i : ℕ
⊢ extend m (s i) = m (s i) ⋯
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

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

Tactic:
ENNReal.iSup_add

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

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
s : ι → Set α
S : Set ι
⊢ ∀ t ∈ piiUnionInter (fun k ↦ {s k}) S, MeasurableSet t

Tactic:
rintro _ ⟨I, hI, f, hf, rfl⟩
    refine Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom ?_
    exact ⟨m, hI hm, (hf m hm).symm⟩

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : (inducedOuterMeasure m P0 m0) s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε

Tactic:
have h := ENNReal.lt_add_right hs hε

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
hs : (inducedOuterMeasure m P0 m0) s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : (inducedOuterMeasure m P0 m0) s < (inducedOuterMeasure m P0 m0) s + ε
⊢ ∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
x : β
hx_empty : C x ∅
hx_basic : ∀ t ∈ s, C x t
hx_compl : ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
⊢ (∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)) →
    ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Tactic:
hx_union

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
x : β
hx_empty : C x ∅
hx_basic : ∀ t ∈ s, C x t
hx_compl : ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
hx_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ i, f i)
⊢ ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
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 α
⊢ sᶜᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] tᶜ

Tactic:
compl_compl

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] tᶜ
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:
simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : ℕ → Set α
p : ℕ → Prop
h : ∀ (n : ℕ), p n → MeasurableSet (s n)
⊢ MeasurableSet (⋂ i, ⋃ j, ⋃ (_ : p j ∧ i ≤ j), s j)
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable β
μ : Measure (α × β)
x : α
⊢ μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}

Tactic:
rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
    preimage_fst_singleton_eq_range]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
⊢ map f μ = map g μ

Tactic:
have hg : AEMeasurable g μ := hf.congr h

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ map f μ = map g μ
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: 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'

Tactic:
rintro ⟨a, has⟩ -
        use a, hsub has
        simp_all [subset_def, le_of_lt]

Goal state after:
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
hsne : s.Nonempty
this : Nonempty ↑s
hsub : ¬s ⊆ Iio b
h : Tendsto Subtype.val atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : ↑⟨c, hcs⟩ ∈ Iio b
hac : ⟨a, has⟩ ≤ ⟨c, hcs⟩
⊢ b ≤ a

Tactic:
simpa using ha

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
⊢ SFinite (sum m)

Tactic:
refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩

Goal state after:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
⊢ IsFiniteMeasure (Function.extend f m 0 n)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x1 x2 ↦ x1 ⊆ x2) fun t ↦ ⋃ i ∈ t, s i
⊢ (μ.restrict (⋃ t, ⋃ i ∈ t, s i)) t = (ν.restrict (⋃ t, ⋃ i ∈ t, s i)) t

Tactic:
simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_biUnion_finset_congr.2 fun i _ => h i]

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

Goal state before:
pp: case iUnion
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, μ s = ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : μ univ = ν univ
s : Set α
this : IsFiniteMeasure ν
f : ℕ → Set α
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), μ (f i) = ν (f i)
⊢ μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
simp [measure_iUnion, hfd, h _ (hfm _), ihf]

Goal state after: