mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ((blimsup (s.piecewise u v) f fun x ↦ x ∈ s) ⊔ blimsup (s.piecewise u v) f fun x ↦ x ∉ s) =
    (blimsup u f fun x ↦ x ∈ s) ⊔ blimsup v f fun x ↦ x ∉ s

Tactic:
refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise u v a = u a

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise u v a = v a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ⊤ ↔ a + ⊤ ≤ c

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

Tactic:
eventually_le_const_iff_forall_gt_eventually_lt_const

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ∀ (b : α), limsup u f < b → ∀ᶠ (x : β) in f, u x < b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
a b : EReal
h : a ≤ b + ⊤
⊢ a - ⊤ ≤ b

Tactic:
| top =>

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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
refine ⟨b', ⟨le_rfl, hb'b⟩, ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)
      filter_upwards [h_lt] with n hn
      contrapose! h
      exact ⟨u n r, h, hn⟩

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

Goal state before:
pp: case top
y : ℝ≥0
h_le : ↑y ≤ ∞
⊢ ↑(∞ - ↑y) = ↑∞ - ↑↑y

Tactic:
| top =>

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
this✝ : x < F.limsSup
this : (Set.Ioo c F.limsSup).Nonempty
⊢ False

Tactic:
simp only [hc, Set.not_nonempty_empty] at this

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
by_cases h : Multipliable f L
  · by_cases hbot : L.NeBot
    · exact h.hasProd.nonneg hf
    · simpa [tprod_bot hbot] using finprod_nonneg hf
  · simp [tprod_eq_one_of_not_multipliable h]

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : IsUniformGroup G
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he

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

Goal state before:
pp: case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x ↦ a
ha : ¬a = 1
⊢ False

Tactic:
have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)

Goal state after:
case refine_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x ↦ a
ha : ¬a = 1
this : {a}ᶜ ∈ 𝓝 1
⊢ False
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 : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun n ↦ if n = b then 1 else f n) a' L
x✝ : β
⊢ update f b 1 x✝ = if x✝ = b then 1 else f x✝

Tactic:
apply update_apply

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

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
⊢ (Multipliable fun n ↦ f ↑n) ↔ Multipliable f

Tactic:
by
  rw [multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| ∏ b ∈ x✝, (fun x ↦ 1 + f x) b

Tactic:
rw [prod_one_add_ordered]

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| 1 + ∑ i ∈ x✝, f i * ∏ j ∈ x✝ with j < i, (1 + f j)
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
x y z : X
⊢ ↑(⨅ l, (zipWith d (x :: l) (l ++ [z])).sum) ≤
    ↑((⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ⨅ l, (zipWith d (y :: l) (l ++ [z])).sum)

Tactic:
NNReal.coe_le_coe

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
x y z : X
⊢ ⨅ l, (zipWith d (x :: l) (l ++ [z])).sum ≤
    (⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ⨅ l, (zipWith d (y :: l) (l ++ [z])).sum
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₄))
x y : X
⊢ ↑(d x y) ≤ ↑(⨅ i, 2 * (zipWith d (x :: i) (i ++ [y])).sum)

Tactic:
NNReal.coe_le_coe

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₄))
x y : X
⊢ d x y ≤ ⨅ i, 2 * (zipWith d (x :: i) (i ++ [y])).sum
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_1
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u

pp: case refine_2
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Tactic:
· obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
    refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H 1 ((f x.fst.fst x.snd)⁻¹ * f x.fst.snd x.snd) ?_
    simpa [dist_eq_norm_inv_mul, norm_div_rev] using hx

Goal state after:
case refine_2
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
| top =>

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

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

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
⊢ Tendsto (fun b ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
⊢ ∃ R, ∃ᶠ (n : ι) in l, R < x n

Tactic:
by
  by_contra! h
  refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
  simp only [eventually_map, ENNReal.coe_le_coe]
  filter_upwards [h (-r)] with i hi using (le_neg.1 hi).trans (neg_le_abs _)

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

Goal state before:
pp: case inl
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top hf
    obtain ⟨q, hq⟩ := exists_rat_gt R
    refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
    · refine fun hcon => hR ?_
      filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
    · simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
      refine fun hcon => hbdd ↑(q + 1) ?_
      filter_upwards [hcon] with x hx using not_lt.1 hx

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✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : UniformContinuousConstSMul M X
x y : M
a : X
⊢ (x * y) • ↑a = x • y • ↑a

Tactic:
simp only [← coe_smul, mul_smul]

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

Goal state before:
pp: ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun i ↦ f i - c) F = limsup f F - c

Tactic:
rcases F.eq_or_neBot with rfl | _
  · simp
  · exact (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|

Tactic:
by
      gcongr ?_ + ?_
      · exact abs_sup_sub_sup_le_abs _ _ _
      · rw [sup_comm c, sup_comm c]
        exact abs_sup_sub_sup_le_abs _ _ _

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

Tactic:
simp [enorm, ENNReal.coe_inv, ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : SeminormedRing α
inst✝⁵ : SeminormedAddGroup β
inst✝⁴ : SMul α β
inst✝³ : NormSMulClass α β
γ : Type u_3
inst✝² : SeminormedAddGroup γ
inst✝¹ : SMul α γ
inst✝ : NormSMulClass α γ
r : α
x✝ : β × γ
v₁ : β
v₂ : γ
⊢ ‖r • (v₁, v₂)‖ = ‖r‖ * ‖(v₁, v₂)‖

Tactic:
by simp only [smul_def, ← coe_nnnorm, nnnorm_def,
    nnnorm_smul r, ← NNReal.coe_mul, NNReal.mul_sup]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
TProd.elim_of_ne _ hji,

Goal state after:
case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ TProd.elim (TProd.mk (i :: is) f).2 ⋯ = f j
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
hy₂ : y ∈ Prod.snd ⁻¹' U
this : r ≤ ‖f y.2‖
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ

Tactic:
have : r / 2 < ‖F y.1 y.2‖ := by
    simp [dist_eq_norm_sub] at hy₁
    linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
hy₂ : y ∈ Prod.snd ⁻¹' U
this✝ : r ≤ ‖f y.2‖
this : r / 2 < ‖F y.1 y.2‖
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K ↔ IsComplete (closedBall 0 1)

Tactic:
by
  constructor <;> intro h
  · exact Metric.isClosed_closedBall.isComplete
  rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _ | ⟨_, rfl⟩
  · rwa [completeSpace_iff_isComplete_univ,
         ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]
  refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_
  obtain ⟨k, hk⟩ := hu.norm_bddAbove
  have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
  obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k
  have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
  have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 := by
    intro
    simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
    rw [div_le_one (kpos.trans_lt hx)]
    exact hx.le.trans' (hk (by simp))
  obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'
  refine ⟨a * x, (((continuous_mul_const x).tendsto a).comp ha').congr ?_⟩
  have hx' : x ≠ 0 := by
    contrapose! hx
    simp [hx, kpos]
  simp [div_mul_cancel₀ _ hx']

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

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ diam (sphere x r) = 2 * r

Tactic:
apply le_antisymm
    (diam_mono sphere_subset_closedBall isBounded_closedBall |>.trans <| diam_closedBall hr)
  obtain ⟨y, hy⟩ := exists_ne (0 : E)
  calc
    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
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
q : 𝕜
x✝ : PUnit.{?u.14 + 1}
⊢ ‖q • x✝‖ ≤ ‖q‖ * ‖x✝‖

Tactic:
by simp only [norm_eq_zero, mul_zero, le_refl]

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

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

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
u : Set ↑s
hs : MeasurableSet (Subtype.val ⁻¹' s)
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' u)

Tactic:
by
  rcases hu with ⟨u, hu, rfl⟩
  convert! (measurable_subtype_coe hu).inter hs
  ext ⟨x, hx⟩
  simpa [@and_comm _ (_ = x)] using and_comm

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ False

Tactic:
rw [← h2, h1] at hx

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y z : β
hx : x ∉ measurableAtom x
hzx : z ∈ measurableAtom x
hzy : z ∈ measurableAtom y
h1 : measurableAtom z = measurableAtom x
h2 : measurableAtom z = measurableAtom y
⊢ False
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
ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
f : ↑(⋃ i, t i) → β := iUnionLift t g' ht' (⋃ i, t i) ⋯
hfm : Measurable f
⊢ ∃ f, Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

Tactic:
refine ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
      hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩

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
ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩
f : ↑(⋃ i, t i) → β := iUnionLift t g' ht' (⋃ i, t i) ⋯
hfm : Measurable f
i : ι
x : α
hx : x ∈ t i
⊢ (fun x ↦ if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x) x = g i x
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

Tactic:
cases lt_irrefl 0 (h₁.trans <| h.trans_lt h₃)

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False

Tactic:
if_neg hn

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if 0 < -a then 1 else if -a < 0 then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Tactic:
Right.neg_pos_iff,

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if -a < 0 then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
⊢ Semicontinuous r ↔ ∀ (b : β), IsOpen[inst✝] {x | r x b}

Tactic:
by
  exact ⟨fun h b ↦ by simpa [isOpen_iff_mem_nhds, Filter.Eventually] using fun x hx ↦ h x b hx,
    fun h x b hbx ↦ (h b).mem_nhds hbx⟩

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

Goal state before:
pp: case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ ↑a * ↑n ≤ ↑m

Tactic:
rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]

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

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

Tactic:
coe_mul,

Goal state after:
case coe_coe
x y : ℝ
⊢ ↑x⁻¹ * ↑y⁻¹ = (↑x)⁻¹ * (↑y)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ ↑(sign ⊤) * (↑⊤.abs)⁻¹ = ⊤⁻¹

Tactic:
| top =>

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

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

Tactic:
rw [← tendsto_coe]
  convert! _root_.tendsto_sum_nat_add fun i => (f i : ℝ)
  norm_cast

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

Goal state before:
pp: case top
⊢ ↑(sign ⊤) * ↑⊤.abs⁻¹ = ⊤⁻¹

Tactic:
| top =>

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

Goal state before:
pp: case top
⊢ ⊥ < ⊤⁻¹

Tactic:
| top =>

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

Goal state before:
pp: case top
⊢ ⊤⁻¹ < ⊤

Tactic:
| top =>

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

Goal state before:
pp: case top
h : 0 ≤ ⊤
⊢ 0 ≤ ⊤⁻¹

Tactic:
| top =>

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

Goal state before:
pp: case top
h : ⊤ ≤ 0
⊢ ⊤⁻¹ ≤ 0

Tactic:
| top =>

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

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']
  rw [mul_div b a b, mul_comm a b]
  exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Goal state after: