mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe
a : ℝ≥0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
| coe a =>

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹.toNNReal = a.toNNReal⁻¹

Tactic:
by
  cases a with
  | top => simp
  | coe a =>
    rcases eq_or_ne a 0 with (rfl | ha); · simp
    rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Tactic:
rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩
  filter_upwards [eventually_closedBall_subset hs] with r hr
  exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Tactic:
by
  rw [sUnion_eq_iUnion] at hc₂; simpa using lebesgue_number_lemma_of_metric hs (by simpa) hc₂

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ |(-(_r - _y))| = ‖-_r + _y‖

Tactic:
neg_sub,

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ |_y - _r| = ‖-_r + _y‖
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
⊢ ∀ᶠ (b : α) in 𝓝[>] x, l < f b

Tactic:
filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
w : α
hw : w ∈ Ioo x y
⊢ l < f w
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
    refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : PseudoEMetricSpace X
d : ℝ≥0∞
⊢ ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

Tactic:
by
  simp only [ediam, iSup_le_iff]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (∃ x y, ¬‖x⁻¹ * y‖₊ = 0) ↔ ∃ x, ‖x‖₊ ≠ 0

Tactic:
exact ⟨fun ⟨x, y, hxy⟩ => ⟨_, hxy⟩, fun ⟨x, hx⟩ => ⟨x, 1, by simpa using hx⟩⟩

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal

Tactic:
rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]

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

Goal state before:
pp: z : ℤ
c : ℝ≥0
⊢ |z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c

Tactic:
by
  rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff zero_le, NNReal.natCast_natAbs z]

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
p : ℚ≥0 × R
| p.1 • p.2

Tactic:
← NNRat.cast_smul_eq_nnqsmul ℚ

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
p : ℚ≥0 × R
| ↑p.1 • p.2
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
· rcases h' with ⟨b, hb⟩
    use b
    intro c hc
    apply hb c
    rw [eventually_map] at hc ⊢
    refine hc.mono (fun _ ↦ ?_)
    simp +contextual only [implies_true, max_le_iff]

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
· rcases h' with ⟨b, hb⟩
    use b
    intro c hc
    apply hb c
    rw [eventually_map] at hc ⊢
    refine hc.mono (fun _ ↦ ?_)
    simp +contextual only [implies_true, max_le_iff]

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, ¬(fun x' ↦ f l ≤ x') x
⊢ ∀ᶠ (x : R) in F, ¬(fun x ↦ l ≤ x) x

Tactic:
simp only [not_le] at ev freq_ge ⊢

Goal state after:
R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
⊢ ∀ᶠ (x : R) in F, x < l
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ x - y ↔ y ≤ x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊥ ↔ ⊥ ≤ ⊥

case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊥ - ↑a✝ ↔ ↑a✝ ≤ ⊥

case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊥ - ⊤ ↔ ⊤ ≤ ⊥

case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊥ ↔ ⊥ ≤ ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ↑a✝¹ - ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ↑a✝ - ⊤ ↔ ⊤ ≤ ↑a✝

case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊥ ↔ ⊥ ≤ ⊤

case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ 0 ≤ ⊤ - ↑a✝ ↔ ↑a✝ ≤ ⊤

case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ 0 ≤ ⊤ - ⊤ ↔ ⊤ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
⊢ x - y ≤ 0 ↔ x ≤ y

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
⊢ ⊥ - ⊥ ≤ 0 ↔ ⊥ ≤ ⊥

case bot.coe
a✝ : ℝ
⊢ ⊥ - ↑a✝ ≤ 0 ↔ ⊥ ≤ ↑a✝

case bot.top
⊢ ⊥ - ⊤ ≤ 0 ↔ ⊥ ≤ ⊤

case coe.bot
a✝ : ℝ
⊢ ↑a✝ - ⊥ ≤ 0 ↔ ↑a✝ ≤ ⊥

case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ - ↑a✝ ≤ 0 ↔ ↑a✝¹ ≤ ↑a✝

case coe.top
a✝ : ℝ
⊢ ↑a✝ - ⊤ ≤ 0 ↔ ↑a✝ ≤ ⊤

case top.bot
⊢ ⊤ - ⊥ ≤ 0 ↔ ⊤ ≤ ⊥

case top.coe
a✝ : ℝ
⊢ ⊤ - ↑a✝ ≤ 0 ↔ ⊤ ≤ ↑a✝

case top.top
⊢ ⊤ - ⊤ ≤ 0 ↔ ⊤ ≤ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
⊢ 0 < x - y ↔ y < x

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
⊢ 0 < ⊥ - ⊥ ↔ ⊥ < ⊥

case bot.coe
a✝ : ℝ
⊢ 0 < ⊥ - ↑a✝ ↔ ↑a✝ < ⊥

case bot.top
⊢ 0 < ⊥ - ⊤ ↔ ⊤ < ⊥

case coe.bot
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊥ ↔ ⊥ < ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
⊢ 0 < ↑a✝¹ - ↑a✝ ↔ ↑a✝ < ↑a✝¹

case coe.top
a✝ : ℝ
⊢ 0 < ↑a✝ - ⊤ ↔ ⊤ < ↑a✝

case top.bot
⊢ 0 < ⊤ - ⊥ ↔ ⊥ < ⊤

case top.coe
a✝ : ℝ
⊢ 0 < ⊤ - ↑a✝ ↔ ↑a✝ < ⊤

case top.top
⊢ 0 < ⊤ - ⊤ ↔ ⊤ < ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ x - y < 0 ↔ x < y

Tactic:
cases x <;> cases y

Goal state after:
case bot.bot
h_top : ⊥ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊥ - ⊥ < 0 ↔ ⊥ < ⊥

case bot.coe
a✝ : ℝ
h_top : ⊥ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊥ - ↑a✝ < 0 ↔ ⊥ < ↑a✝

case bot.top
h_top : ⊥ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊥ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊥ - ⊤ < 0 ↔ ⊥ < ⊤

case coe.bot
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ↑a✝ - ⊥ < 0 ↔ ↑a✝ < ⊥

case coe.coe
a✝¹ a✝ : ℝ
h_top : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ↑a✝¹ - ↑a✝ < 0 ↔ ↑a✝¹ < ↑a✝

case coe.top
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ↑a✝ - ⊤ < 0 ↔ ↑a✝ < ⊤

case top.bot
h_top : ⊤ ≠ ⊤ ∨ ⊥ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊥ ≠ ⊥
⊢ ⊤ - ⊥ < 0 ↔ ⊤ < ⊥

case top.coe
a✝ : ℝ
h_top : ⊤ ≠ ⊤ ∨ ↑a✝ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ↑a✝ ≠ ⊥
⊢ ⊤ - ↑a✝ < 0 ↔ ⊤ < ↑a✝

case top.top
h_top : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊥
⊢ ⊤ - ⊤ < 0 ↔ ⊤ < ⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ⨅ i ∈ f, g (⨆ b, ⨆ (_ : p b ∧ b ∈ i), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)

Tactic:
simp only [_root_.map_iSup, le_refl]

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

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
· rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
      Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]
    exact neg_nonneg.2 h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
hL : L.filter.NeBot
⊢ L.NeBot

Tactic:
exact ⟨hL⟩

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

Goal state before:
pp: case top.coe.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
· simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a ((unconditional β).comap { toFun := g, inj' := hg })

Tactic:
SummationFilter.comap_unconditional

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ ∀ᶠ (x' : Finset β) in L.filter, ∏ b ∈ x', f b = ∏ b ∈ L.support.toFinset, f b

Tactic:
have h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem L.support.toFinite).mpr (by tauto)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter
⊢ ∀ᶠ (x' : Finset β) in L.filter, ∏ b ∈ x', f b = ∏ b ∈ L.support.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c

Tactic:
extend_apply' _ _ _ h

Goal state after:
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ 1 c ≤ g c
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ edist (Pi.single i x) (Pi.single i y) = edist x y

Tactic:
rw [edist_pi_def]

Goal state after:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ (Finset.univ.sup fun b ↦ edist (Pi.single i x b) (Pi.single i y b)) = edist x y
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal) ↔ Tendsto f u (𝓝 a)

Tactic:
refine ⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩

Goal state after:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto f u (𝓝 a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case coe
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : ↑a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ ↑a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))

Tactic:
| coe a =>

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
⊢ UniformContinuous (extend f)

Tactic:
by
  by_cases hf : UniformContinuous f
  · rw [extend, if_pos hf]
    exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf
  · rw [extend, if_neg hf]
    exact uniformContinuous_of_const fun a _b => by congr

Goal state after:
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
⊢ Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (g i)) atTop (𝓝 b)

Tactic:
by simpa [← hg] using sum_v

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x = n • m • x

Tactic:
hnm,

Goal state after:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x =
    (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y ∈ Icc (f x - ε) (f x + ε)

Tactic:
refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩ <;> grw [← hδ.le]

Goal state after:
case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + C * ↑δ

case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + C * ↑δ
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:

Tactic:
sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
    _ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove)
        (csInf_mem_closure hne h.bddBelow)

Goal state after:
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 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ dist (a • b) (x • y) ≤ ε

Tactic:
dist_triangle _ (a • y),

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 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ dist (a • b) (a • y) + dist (a • y) (x • y) ≤ ε
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mpr.inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h : 1 ≤ ‖x‖
⊢ ‖x‖ = 1

pp: 𝕜✝ : Type u_5
inst✝² : NormedDivisionRing 𝕜✝
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
⊢ ‖x‖ = 1

Tactic:
· rcases h.eq_or_lt with h | h
      · rw [h]
      replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
      rw [← inv_inj, inv_one, ← norm_inv]
      exact H (by simpa) h' h

Goal state after:
𝕜✝ : Type u_5
inst✝² : NormedDivisionRing 𝕜✝
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
⊢ ‖x‖ = 1
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 : α
⊢ nndist (f x) (f y) = ratio f * nndist x y

Tactic:
by
  simp only [← ENNReal.coe_inj, ← edist_nndist, ENNReal.coe_mul, edist_eq]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : v (-x + y) = 0
⊢ x = y

Tactic:
rw [add_comm, ← sub_eq_add_neg, AbsoluteValue.map_sub_eq_zero_iff] at hxy

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y : R
hxy : y = x
⊢ x = y
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
n : ℕ∞
⊢ MeasurableSet (f ⁻¹' {n})

Tactic:
cases n with

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

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

Tactic:
← preimage_compl,

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0

Tactic:
by
  rw [← sUnion_range, measure_sUnion_null_iff (countable_range s), forall_mem_range]

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

Goal state before:
pp: α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
x y : SignType
⊢ ↑(x * y) = ↑x * ↑y

Tactic:
cases x <;> cases y

Goal state after:
case zero.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * zero) = ↑zero * ↑zero

case zero.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * neg) = ↑zero * ↑neg

case zero.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * pos) = ↑zero * ↑pos

case neg.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * zero) = ↑neg * ↑zero

case neg.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * neg) = ↑neg * ↑neg

case neg.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * pos) = ↑neg * ↑pos

case pos.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * zero) = ↑pos * ↑zero

case pos.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * neg) = ↑pos * ↑neg

case pos.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * pos) = ↑pos * ↑pos
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ Summable f

Tactic:
refine ⟨a, ENNReal.hasSum_coe.1 ?_⟩

Goal state after:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a ↦ ↑(f a)) ↑a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y → x = y

Tactic:
rintro ⟨habs, hsign⟩
    rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]

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

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

Tactic:
| coe a =>

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

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

Tactic:
| coe a =>

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

Goal state before:
pp: case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ (↑a)⁻¹

Tactic:
| coe a =>

Goal state after: