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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
R : ℝ
R0 : R > 0
H : ∀ (n : ℕ), dist (u n) (u N) < R
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
⊢ ∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R

Tactic:
· exact ⟨_, add_pos R0 R0, fun m n =>
      lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
⊢ ∃ R > 0, ∀ (n : ℕ), dist (u n) (u N) < R
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ = ‖x‖

Tactic:
rw [div_eq_mul_inv, norm_mul_eq_norm_left]

Goal state after:
case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k : ℕ
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → ∀ m ≥ b_1, dist (u m) (u b_1) < b k

Tactic:
obtain ⟨N, hN⟩ := hu (b k) (hb k)

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < b k
⊢ ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → ∀ m ≥ b_1, dist (u m) (u b_1) < b k
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n ↦ ↑(f n)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]; rfl

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (none, b)

pp: case some
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, b)

Tactic:
· exact tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, b)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

case cons
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
a✝¹ : κ
s✝ : Finset κ
h✝ : a✝¹ ∉ s✝
a✝ : (∀ k ∈ s✝, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s✝, u k)
h : ∀ k ∈ Finset.cons a✝¹ s✝ h✝, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons a✝¹ s✝ h✝, u k)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q

Tactic:
simp only [blimsup_eq]
  congr with a
  refine eventually_congr (h.mono fun b hb => ?_)
  rcases eq_or_ne (u b) ⊥ with hu | hu; · simp [hu]
  rw [hb hu]

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

Goal state before:
pp: a : EReal
b : ℝ
⊢ ↑b - (↑b + a) = -a

Tactic:
rw [add_comm, sub_add_cancel_right]

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

Goal state before:
pp: x y : EReal
⊢ (x * y).toReal = x.toReal * y.toReal

Tactic:
induction x, y using induction₂_symm with
  | top_zero => simp
  | zero_bot => simp
  | top_top => simp
  | top_bot => simp
  | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg h]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
⊢ map Finset.card atTop = atTop

Tactic:
map_atTop_eq,

Goal state after:
α : Type u_3
inst✝ : Infinite α
⊢ ⨅ a, 𝓟 (Finset.card '' {a' | a ⊆ a'}) = atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
hb : ¬∀ᶠ (s : Finset β) in L.filter, b ∈ s
⊢ ∀ᶠ (s : Finset β) in L.filter, b ∉ s

Tactic:
filter_upwards [L.eventually_le_support] with a ha using notMem_subset ha hb

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 : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (x : β), f x = ∏' (y : γ), g y

Tactic:
rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf]
  simp only [hfg]

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

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

Tactic:
by
      simp only [update, if_true, eq_rec_constant, dite_eq_ite]

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

Goal state before:
pp: case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
· exact iSup_pow hf _

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hus : ∀ (n : ℕ), u n ∈ f '' s
hu : Tendsto u atTop (𝓝 (f x))
⊢ x ∈ seqClosure s

Tactic:
choose v hv hvu using hus

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : ℕ → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ x ∈ seqClosure s
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 : ℕ
hm : Forall₂ (fun x y ↦ d x y = 0) (x :: l) (l ++ [y])
hLm : L.length ≤ m
⊢ False

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 : ℕ
hm : Forall (fun x ↦ x = 0) L
hLm : L.length ≤ m
⊢ (x :: l).length = (l ++ [y]).length

Tactic:
← isChain_cons_append_singleton_iff_forall₂

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 : ℕ
hm : List.IsChain (fun x y ↦ d x y = 0) (x :: l ++ [y])
hLm : L.length ≤ m
⊢ False

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 : ℕ
hm : Forall (fun x ↦ x = 0) L
hLm : L.length ≤ m
⊢ (x :: l).length = (l ++ [y]).length
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b x : α
hx : x ∈ Iic b
y : α
hy : y ∈ Iic b
hxy : x < y
⊢ projIic b x < projIic b y

Tactic:
simpa only [projIic_of_mem, hx, hy]

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

Goal state before:
pp: s : Set ℝ
h : Bornology.IsBounded s
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)
  · simp
  refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_
  · exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)
  · apply ENNReal.ofReal_le_of_le_toReal
    rw [← Metric.diam, ← Metric.diam_closure]
    calc 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.Instances.ENNReal.Lemmas

Goal state before:
pp: t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ ∀ (x : ℝ≥0∞), min t x ∈ {a | a ≠ ∞}

Tactic:
simp [t_ne_top]

Goal state after:
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)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ n, (x₁, x₄) ∉ U n
h₁₂ : (x₁, x₂) ∈ U (Nat.find H + 1)
h₂₃ : (x₂, x₃) ∈ U (Nat.find H + 1)
h₃₄ : (x₃, x₄) ∈ U (Nat.find H + 1)
⊢ (x₁, x₄) ∈ U (Nat.find H + 1) ○ (U (Nat.find H + 1) ○ U (Nat.find H + 1))

Tactic:
exact ⟨x₂, h₁₂, x₃, h₂₃, h₃₄⟩

Goal state after:
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
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun a ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)

Tactic:
rw [key]

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
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun a ↦ b.truncateToReal (u a)) f = liminf (b.truncateToReal ∘ u) f
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
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
⊢ limsup (fun a ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)

Tactic:
rw [key]

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
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
⊢ limsup (fun a ↦ b.truncateToReal (u a)) f = limsup (b.truncateToReal ∘ u) f
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (b * a) a = ‖b‖

Tactic:
rw [dist_comm, dist_mul_self_right]

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

Goal state before:
pp: case mpr.inr.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‖
h : ‖x⁻¹‖ < 1
⊢ ‖x⁻¹‖ = 1

Tactic:
exact H (by simpa) h' h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Dilation.id α) = 1

Tactic:
rcases h with ⟨x, y, hne⟩
    refine (ratio_unique hne.1 hne.2 ?_).symm
    simp

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 : α × α
⊢ Tendsto (fun e ↦ ‖e.1 * e.2 - (fun p ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)

Tactic:
by
        have : ∀ e : α × α,
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := by
          intro e
          calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
        refine squeeze_zero (fun e => norm_nonneg _) this ?_
        convert!
          ((continuous_fst.tendsto x).norm.mul
                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)
        simp

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n

Tactic:
simpa only [NNReal.coe_pow, coe_nnnorm] using NNReal.coe_mono (nnnorm_pow_le' a h)

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

Goal state before:

Tactic:
2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) := by
      simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, hy, mul_assoc]
    _ ≤ diam (sphere x r) := by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]

Goal state after:
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 : E
⊢ ‖-x + x‖ = 0

Tactic:
show ‖-x + x‖ = 0

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 : E
⊢ ‖-x + x‖ = 0
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 : E
⊢ ‖0‖ = 0

Tactic:
have : (0 : E) = (0 : 𝕜) • (0 : E) := by simp

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 : E
this : 0 = 0 • 0
⊢ ‖0‖ = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ inclusion h '' Subtype.val ⁻¹' u ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s

Tactic:
simpa [@and_comm _ (_ = x)] using and_comm

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

Goal state before:
pp: ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑ i ∈ s, f i + ∑' (i : ↑(↑s)ᶜ), f ↑i = ∑' (i : ι), f i

Tactic:
by
  rw [tsum_subtype, sum_eq_tsum_indicator]
  simp [← ENNReal.tsum_add]

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

Goal state before:
pp: case top_neg
x : ℝ
x_neg : x < 0
⊢ (⊤ * ↑x)⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
top_mul_of_neg (EReal.coe_neg'.2 x_neg),

Goal state after:
case top_neg
x : ℝ
x_neg : x < 0
⊢ ⊥⁻¹ = ⊤⁻¹ * (↑x)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : EReal
⊢ x⁻¹ < ⊤

Tactic:
by
  cases x with
  | bot => exact inv_bot ▸ zero_lt_top
  | top => exact EReal.inv_top ▸ zero_lt_top
  | coe x => exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)

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

Goal state before:
pp: case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Tactic:
mul_top_of_pos a0'

Goal state after:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < ⊤
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
have b0 : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha

Goal state after:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅ ↔ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

Tactic:
by
  refine ⟨fun H ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
  · suffices ∀ i ∈ I, IsClosed (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i) by
      simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H
    exact fun i hi ↦ lowerSemicontinuous_restrict_iff.mpr (hfi i hi) |>.isClosed_preimage c
  · rw [Set.eq_empty_iff_forall_notMem]
    simp only [mem_inter_iff, mem_iInter, mem_preimage, mem_Iic, not_and, not_forall,
      exists_prop, not_le]
    grind

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h' : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝¹, ↑a✝)

Tactic:
exact continuousAt_add_coe_coe _ _

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

Goal state before:
pp: ⊢ ∑' (m : ℕ), (2 ^ (m + 1))⁻¹ = 1

Tactic:
ENNReal.inv_pow,

Goal state after:
⊢ ∑' (m : ℕ), 2⁻¹ ^ (m + 1) = 1
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x

Tactic:
· simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' ↦ ⨆ i, f i x') s x
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ a ∈ f ⁻¹' v

Tactic:
apply hu

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ f a ∈ Ico (f x) u
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S

Tactic:
by
  induction h with
  | base h_s => exact h_s
  | inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
s : ι → Set α
h : ∀ (i : ι), m.IsCaratheodory (s i)
i : ι
⊢ m.IsCaratheodory ((partialSups s) i)

Tactic:
simpa only [partialSups_apply, Finset.sup'_eq_sup, Finset.sup_set_eq_biUnion, ← Finset.mem_coe,
    Finset.coe_Iic] using .biUnion_of_finite (finite_Iic _) (fun j _ ↦ h j)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ (∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩) →
    ∀ (a_2 : β) (b : a_2 ∈ s), ⟨a_2, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_2, b⟩

Tactic:
intro h1

Goal state after:
case refine_1.mp
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ f ⟨a_1, b⟩
⊢ ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) ↑⟨a_1, b⟩