mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
try {· simp}

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
try {· simp}

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

Goal state before:
pp: case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Tactic:
· exact add_lt_add h hlt

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n

Tactic:
by
  rw [iterate_succ, mul_comm]
  simpa only [ENNReal.coe_pow] using! (hf.iterate n) x (f x)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∈ m
⊢ j = liminfReparam f s p j

Tactic:
simp only [m, liminfReparam, hj, ite_true]

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

Goal state before:
pp: case inr
y z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (y + z) = ↑x * y + ↑x * z

Tactic:
cases y <;> cases z <;>
    simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul, ← coe_add, mul_add]

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

Goal state before:
pp: x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ (y + z) * x = y * x + z * x

Tactic:
by
  simpa only [EReal.mul_comm] using left_distrib_of_nonneg_of_ne_top hx_nonneg hx_ne_top y z

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst✝⁶, inst✝⁴] ⇑g
hg' : Continuous[inst✝⁴, inst✝⁶] ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f) L
this : Multipliable ((⇑g' ∘ ⇑g) ∘ f) L
⊢ Multipliable f L

Tactic:
hinv.id

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : CommMonoid α
inst✝⁶ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝⁵ : CommMonoid γ
inst✝⁴ : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst✝³ : FunLike G α γ
inst✝² : MonoidHomClass G α γ
inst✝¹ : FunLike G' γ α
inst✝ : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst✝⁶, inst✝⁴] ⇑g
hg' : Continuous[inst✝⁴, inst✝⁶] ⇑g'
hinv : LeftInverse ⇑g' ⇑g
h : Multipliable (⇑g ∘ f) L
this : Multipliable (id ∘ f) L
⊢ Multipliable f L
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j = ∏' (k : ℕ), f (k + i)

Tactic:
rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
b' : β
⊢ (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1

Tactic:
split_ifs with hb'

Goal state after:
case pos
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
b' : β
hb' : b' = b
⊢ f b' * x = update f b x b' * f b

case neg
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
b' : β
hb' : ¬b' = b
⊢ f b' * 1 = update f b x b' * 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Goal state after:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
⊢ Summable fun x ↦ ∑' (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Tactic:
simp only [bot_lt_iff_ne_bot]

Goal state after:
⊢ ⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + ∑' (b : ι), -f b * ∏ i < b, (1 + -f i)

Tactic:
exact tprod_one_add_ordered hsum' hprod

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

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
← tendsto_coe,

Goal state after:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun a ↦ ↑(∑' (b : { x // x ∉ a }), f ↑b)) atTop (𝓝 ↑0)
Module: Mathlib.Topology.MetricSpace.Isometry

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

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

Goal state after:
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 ≠ ∞
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto ((fun x ↦ ↑x) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)

Tactic:
exact (tendsto_coe_toNNReal ha).comp h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ bs, f p) atTop (𝓝 (∏ b ∈ bs, g b))

Tactic:
simp only [← sigma_preimage_mk, prod_sigma]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (fun t ↦ ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ bs, g b))
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: 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
⊢ M < L.length

Tactic:
rwa [hL_len, Nat.lt_succ_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
⊢ Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ t0, f p) atTop (𝓝 (∏ b ∈ t0, g b))

Tactic:
simp only [← sigma_preimage_mk, prod_sigma]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst✝¹.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image Sigma.fst s ⊆ t0
⊢ Tendsto (fun t ↦ ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk a) ⋯, f ⟨a, s⟩) atTop (𝓝 (∏ b ∈ t0, g b))
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)
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
have mem_𝓤 : ∀ n, { p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1) } ∈ 𝓤 E := fun n => by
    simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)

Goal state after:
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)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: 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
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) =
    zipWith d (x :: take M l) (take M (l ++ [y]) ++ (l ++ [y])[M]?.toList)

Tactic:
getElem?_append_left hMl,

Goal state after:
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
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) =
    zipWith d (x :: take M l) (take M (l ++ [y]) ++ l[M]?.toList)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
γ : Type uγ
inst✝ : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
e : α ≃ᵤ β
⊢ pkg'.map pkg ⇑e.symm ∘ pkg.map pkg' ⇑e = id

Tactic:
by
    simp [map_comp _ _ _ e.symm.uniformContinuous e.uniformContinuous]

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

Goal state before:
pp: case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk a) = a

Tactic:
refine induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_

Goal state after:
case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion α
a : α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk ↑a) = ↑a
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = ⟨a, ⋯⟩

Tactic:
by
  simp [projIcc, hx, hx.trans h]

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 α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧ dist (f y) (F n y) + dist (f y) 0 < C + 1 ∧ dist (G n y) 0 < C + 1

Tactic:
dist_triangle_left (G n y) 0 (g y)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧
    dist (f y) (F n y) + dist (f y) 0 < C + 1 ∧ dist (g y) (G n y) + dist (g y) 0 < C + 1
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ ≤ A * δ * C

Tactic:
by gcongr; exact hg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖

Tactic:
rw [mul_sub, sub_mul, sub_add_sub_cancel]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1

Tactic:
exact lt_add_of_le_of_pos hx zero_lt_one

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ (‖(↑a - 1) * (↑b - 1)‖ + ‖(↑b - 1) * (↑a - 1)‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ ≤
    (‖↑a - 1‖ * ‖↑b - 1‖ + ‖↑b - 1‖ * ‖↑a - 1‖) * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
gcongr <;> exact norm_mul_le ..

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

Goal state before:
pp: R : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Finite ι
inst✝³ : Finite ι'
F : Type u_8
inst✝² : FunLike F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
⊢ ⨆ a, v (x a.1 * y a.2) = ⨆ i, ⨆ i_1, v (x i) * v (y i_1)

Tactic:
map_mul,

Goal state after:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Finite ι
inst✝³ : Finite ι'
F : Type u_8
inst✝² : FunLike F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
⊢ ⨆ a, v (x a.1) * v (y a.2) = ⨆ i, ⨆ i_1, v (x i) * v (y i_1)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case pos
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // h'.toNormedField = h }

Tactic:
exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩

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 (s₁ ∩ s₂)

Tactic:
rw [inter_eq_compl_compl_union_compl]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
⊢ ‖-x + z‖ ≤ ‖-x + y‖ + ‖-y + z‖

Tactic:
have : -x + z = (-x + y) + (-y + z) := by abel

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + z‖ ≤ ‖-x + y‖ + ‖-y + z‖
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
μ₁ μ₂ : OuterMeasure α
h : ∀ (s : Set α), s.Nonempty → μ₁ s = μ₂ s
s : Set α
he : s = ∅
⊢ μ₁ s = μ₂ s

Tactic:
by simp [he]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
i j : ι
x : α
⊢ ∀ (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩

Tactic:
hxi

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
i j : ι
x : α
hxi : x ∈ t i
⊢ ∀ (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∃ i, p i a}

Tactic:
rw [ofPred_exists]

Goal state after:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋃ i, {x | p i x})
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (i : ι) (x : ↑(t i)), f ↑x

Tactic:
nth_rw 2 [← tsum_univ]

Goal state after:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑univ) (x_1 : ↑(t ↑x)), f ↑x_1
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
· have A := tsum_eq_zero_of_not_summable h
    simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h
    simp only [h, ENNReal.toNNReal_top, A]

Goal state after: