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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
⊢ (CauchySeq fun s ↦ ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
by
  refine cauchySeq_finset_iff_tprod_vanishing.trans ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
  · obtain ⟨s, hs⟩ := vanish e he
    refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
    split_ifs at ht with h
    · exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)
    · exact fun _ _ hs ↦ h ⟨_, hs⟩
  · obtain ⟨N, hN⟩ := vanish e he
    exact ⟨range N, fun t ht ↦ hN _ fun n hnt ↦
      le_of_not_gt fun h ↦ Set.disjoint_left.mp ht hnt (mem_range.mpr h)⟩

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

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

Tactic:
hg y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ ↑K * edist x y
⊢ edist (g x) (g y) ≤ ↑K * edist x y
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)

Tactic:
nth_rewrite 2 [← coe_toNNReal ha]
  exact continuous_coe.tendsto _

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ Tendsto (fun a ↦ ‖a‖) (𝓝 x) (𝓝 ‖x‖)

Tactic:
by
  simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)

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

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

Tactic:
rw [extend_def _ h.uniformContinuous]

Goal state after:
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
⊢ f ∈ closure (range pureCauchy)

Tactic:
by
  have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
    let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
    let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
    have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
    let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
    let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
    have : t'' ∈ f.val ×ˢ pure x :=
      mem_prod_iff.mpr
        ⟨t, ht, { y : α | (x, y) ∈ t' }, h <| mk_mem_prod hx hx,
          fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
          ht'₂ <| SetRel.prodMk_mem_comp (@h (a, x) ⟨h₁, hx⟩) h₂⟩
    ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩
  simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
    Set.inter_comm _ (range pureCauchy), mem_ofPred_eq]
  refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
  · exact monotone_const.inter monotone_preimage
  · let ⟨y, hy⟩ := h_ex s hs
    have : pureCauchy y ∈ range pureCauchy ∩ { y : CauchyFilter α | (f, y) ∈ s } :=
      ⟨mem_range_self y, hy⟩
    exact ⟨_, this⟩

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

Goal state before:
pp: case mp
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
⊢ Nonempty α

pp: case mpr
α : Type u
inst✝ : UniformSpace α
c : α
⊢ Nonempty (CauchyFilter α)

Tactic:
· have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c
    obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
    exact ⟨a⟩

Goal state after:
case mpr
α : Type u
inst✝ : UniformSpace α
c : α
⊢ Nonempty (CauchyFilter α)
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
liminf_le : liminf u f ≤ b
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)

Tactic:
filter_upwards [le_b] with i i_le_b

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
i : ι
i_le_b : u i ≤ b
⊢ (u i).toReal = b.truncateToReal (u i)
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
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)

Tactic:
filter_upwards [le_b] with i i_le_b

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
i : ι
i_le_b : u i ≤ b
⊢ (u i).toReal = b.truncateToReal (u i)
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε

Tactic:
rw [Prod.dist_eq, max_le_iff] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x✝¹ x✝ : α × β
a : α
b : β
hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b).1 (x, y).1 ≤ ε / (2 * C) ∧ dist (a, b).2 (x, y).2 ≤ ε / (2 * C)
⊢ dist (Function.uncurry (fun x1 x2 ↦ x1 • x2) (a, b)) (Function.uncurry (fun x1 x2 ↦ x1 • x2) (x, y)) ≤ ε
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : SeminormedGroup E
inst✝³ : SeminormedGroup F
inst✝² : FunLike 𝓕 E F
inst✝¹ : IsometryClass 𝓕 E F
inst✝ : OneHomClass 𝓕 E F
f : 𝓕
x : E
⊢ ‖f x‖ₑ = ‖x‖ₑ

Tactic:
by simp [enorm]

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)

Tactic:
mul_assoc,

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)
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
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∃ x, ∀ y ∈ Set.range fun n ↦ ‖u n‖, y ≤ x

Tactic:
exact ⟨C + ‖u 0‖, by simpa using this⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio e.symm * ratio e = 1

Tactic:
← ratio_trans,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio (e.symm.trans e) = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
inst✝² : SeminormedAddCommGroup G
inst✝¹ : One G
inst✝ : NormOneClass G
⊢ ‖1‖ₑ = 1

Tactic:
by simp [enorm]

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

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

Tactic:
by simp [enorm]

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

Goal state before:
pp: α : Type u_2
inst✝² : SeminormedAddCommGroup α
inst✝¹ : Mul α
inst✝ : NormMulClass α
a b : α
⊢ ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ

Tactic:
by simp [enorm]

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

Goal state before:
pp: α : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormMulClass α
a : α
n : ℕ
⊢ ‖a ^ n‖ₑ = ‖a‖ₑ ^ n

Tactic:
by simp [enorm]

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}
⊢ MeasurableSet {x | p x ↔ q x}

Tactic:
have h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x} := by ext; simp; grind
  rw [h_eq]
  exact (hs.imp ht).inter (ht.imp hs)

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⨆ i, t i) ≤ ∑' (i : ℕ), μ (t i)

Tactic:
calc
    μ (⋃ i, t i) = μ (⋃ i, disjointed t i) := by rw [iUnion_disjointed]
    _ ≤ ∑' i, μ (disjointed t i) :=
      OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _)
    _ ≤ ∑' i, μ (t i) := by gcongr; exact disjointed_subset ..

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

Goal state before:
pp: case neg
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : ∀ (i : Set β), y ∈ i → MeasurableSet i → x ∈ i
s : Set β
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
⊢ False

Tactic:
specialize hx sᶜ hys hs.compl

Goal state after:
case neg
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
s : Set β
hx : x ∈ sᶜ
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
⊢ False
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ c • m (⋃ i, s i) ≤ ∑' (i : ℕ), c • m (s i)

Tactic:
by
        simp_rw [← smul_one_mul c (m _), ENNReal.tsum_mul_left]
        exact mul_right_mono (measure_iUnion_le _)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Tactic:
rw [← coe_id, coe_inj]

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

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

pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i

Tactic:
← ENNReal.tsum_eq_iSup_nat

Goal state after:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe_coe
x y : ℝ
⊢ ↑x⁻¹ * ↑y⁻¹ = (↑x)⁻¹ * (↑y)⁻¹

Tactic:
coe_inv,

Goal state after:
case coe_coe
x y : ℝ
⊢ (↑x)⁻¹ * ↑y⁻¹ = (↑x)⁻¹ * (↑y)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
← tendsto_coe

Goal state after:
f : ℕ → ℝ≥0
⊢ Tendsto (fun a ↦ ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x : ↑s
this : pure ↑x ≤ φ (f ↑x)
⊢ (φ (f ↑x)).NeBot

Tactic:
exact neBot_of_le this

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

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

Tactic:
rw [range_coe_eq_Ioo]

Goal state after:
⊢ (Ioo ⊥ ⊤).OrdConnected
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case neg
x✝¹ : ℝ
hx : ↑x✝¹ < ⊤
hx_bot : ¬↑x✝¹ = ⊥
x : EReal
x✝ : x ∈ Ico ↑x✝¹ ⊤
h1 : ↑x✝¹ ≤ x
h2 : x < ⊤
⊢ x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ

Tactic:
simp [h1, h2.ne_top]

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

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

Tactic:
by
  rw [tendsto_nhds_top_iff_real, atTop_basis_Ioi.tendsto_right_iff]; simp

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

Goal state before:
pp: case neg
x : EReal
h_top : ¬x = ⊤
⊢ ContinuousOn toENNReal {⊤}ᶜ

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx ↦ ?_).congr (fun _ h ↦ toENNReal_of_ne_top h)

Goal state after:
case neg
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
⊢ ContinuousAt (fun x ↦ ENNReal.ofReal x.toReal) x
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
by
  rcases lt_or_ge r 1 with hr | hr
  · rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
    norm_cast at *
    convert! ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
    rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
  · rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
    refine fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_
    calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * (C * 2⁻¹ ^ n)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
by
  rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩
  rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩
  rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩
  exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩

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

Goal state before:
pp: k : ℕ
hn : 0 < k.succ
⊢ (∏ x ∈ Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹

Tactic:
refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;>
          intro x hx

Goal state after:
case refine_1
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹

case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
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)
⊢ m (⋃ i, s i) = ∑' (i : ℕ), m (s i)

Tactic:
refine le_antisymm (measure_iUnion_le s) ?_
  rw [ENNReal.tsum_eq_iSup_nat]
  refine iSup_le fun n => ?_
  have := @isCaratheodory_sum _ m _ h hd univ n
  simp only [inter_comm, inter_univ, univ_inter] at this; simp only [this]
  exact m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
by
    by_cases ht : a ∈ t; swap; · simp [ht]
    by_cases hs : a ∈ s <;> simp [*]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
⊢ piiUnionInter π {i} = π i ∪ {univ}

Tactic:
ext1 s
  simp only [piiUnionInter, exists_prop, mem_union]
  refine ⟨?_, fun h => ?_⟩
  · rintro ⟨t, hti, f, hfπ, rfl⟩
    simp only [subset_singleton_iff, Finset.mem_coe] at hti
    by_cases hi : i ∈ t
    · have ht_eq_i : t = {i} := by
        ext1 x
        rw [Finset.mem_singleton]
        exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
      simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]
      exact Or.inl (hfπ i hi)
    · have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
      simp [ht_empty, iInter_univ, Set.mem_singleton univ]
  · rcases h with hs | hs
    · refine ⟨{i}, ?_, fun _ => s, ⟨fun x hx => ?_, ?_⟩⟩
      · rw [Finset.coe_singleton]
      · rw [Finset.mem_singleton] at hx
        rwa [hx]
      · simp only [Finset.mem_singleton, iInter_iInter_eq_left]
    · refine ⟨∅, ?_⟩
      simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
        imp_true_iff, Finset.notMem_empty, iInter_false, iInter_univ, true_and,
        exists_const] using! hs

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : (⋂ i ∈ p1 ∪ p2, g i).Nonempty
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ ⋂ (_ : n ∈ p1 ∪ p2), g n ⊆ ∅

Tactic:
refine Set.iInter_subset_of_subset hn ?_

Goal state after:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : (⋂ i ∈ p1 ∪ p2, g i).Nonempty
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ g n ⊆ ∅
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ∞
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ∞

Tactic:
· simpa only [ENNReal.sum_lt_top, Finite.mem_toFinset]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}

Tactic:
piiUnionInter_singleton

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case mp
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x ↦ x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
rintro ⟨x, rfl⟩
    by_cases hT : True ∈ x
    · by_cases hF : False ∈ x
      · suffices x = univ by grind
        grind [univ_eq_true_false]
      · grind
    · by_cases hF : False ∈ x
      · grind
      · suffices x ⊆ ∅ by grind
        intro p hp
        fin_cases p <;> contradiction

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ m (⋃ i, disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯

Tactic:
rw [mU (MeasurableSet.disjointed h) (disjoint_disjointed _)]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ ∑' (i : ℕ), m (disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
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 t ≤ μ t'

Tactic:
inter_subset

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)
⊢ ((restrict s) μ).trim t ≤ μ t'
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ k ≤ φ (succ k)

Tactic:
specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl
    nth_grw 1 [ih]
    refine succ_le_of_lt (hφ (le_succ _) le_rfl ?_)
    exact lt_succ_of_not_isMax hk

Goal state after:
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case inl
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hb' : Iio b = ∅
this : IsEmpty ↑s
⊢ map Subtype.val ⊥ = 𝓝[<] b

Tactic:
Filter.map_bot,

Goal state after:
case inl
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hb' : Iio b = ∅
this : IsEmpty ↑s
⊢ ⊥ = 𝓝[<] b