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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
⊢ StrictMonoOn f (Icc a b)

Tactic:
refine StrictMono.of_domRestrict ?_

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
⊢ StrictMono ((Icc a b).domRestrict f)
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ (∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal

Tactic:
ENNReal.toReal,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ↑(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
y : ι
y_0 : 0 ≤ u y
y_U : u y ≤ U
⊢ 0 ≤ U

Tactic:
exact y_0.trans y_U

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

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop ≠ ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
    exact tendsto_atTop_isLUB h_mono <|
      h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

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

Goal state before:
pp: case inr
ι : 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 : ι
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)

Tactic:
refine tendsto_order.mpr ⟨fun b hb ↦ ?_, fun b hb ↦ ?_⟩

Goal state after:
case inr.refine_1
ι : 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_1 : α) in atTop, b < ⨆ i, u i b_1

case inr.refine_2
ι : 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_1 : α) in atTop, ⨆ i, u i b_1 < b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ (∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y) → ∀ ⦃c : β⦄, x < c → limsup u f < c

Tactic:
intro h y x_y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
y : β
x_y : x < y
⊢ limsup u f < y
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
by_cases! H : ∃ j, j ∈ m

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
H : ∃ j, j ∈ m
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
H : ∀ (j : Subtype p), j ∉ m
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case a
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
⊢ f F.limsSup ≤ liminf f F

Tactic:
rw [limsSup, f_decr.map_csInf_of_continuousAt f_cont bdd_above cobdd]
    apply le_of_forall_lt
    intro c hc
    simp only [liminf, limsInf, eventually_map] at hc ⊢
    obtain ⟨d, hd, h'd⟩ :=
      exists_lt_of_lt_csSup (bdd_above.recOn fun x hx ↦ ⟨f x, Set.mem_image_of_mem f hx⟩) hc
    apply lt_csSup_of_lt ?_ ?_ h'd
    · simpa only [BddAbove, upperBounds]
        using! Antitone.isCoboundedUnder_ge_of_isCobounded f_decr cobdd
    · rcases hd with ⟨e, ⟨he, fe_eq_d⟩⟩
      filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)

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 : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L

Tactic:
by
  apply tendsto_nhds_of_eventually_eq
  have h1 : ⋂ b ∈ (↑s ∩ L.support), {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem (Set.toFinite _)).mpr (fun b hb ↦ hb.2)
  filter_upwards [h1, L.eventually_le_support] with t ht ht'
  simp only [Set.mem_iInter] at ht
  apply Finset.prod_congr_of_eq_on_inter <;> grind

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ a, ∀ (b : Finset α), a ⊆ b → ∏' (a : { x // x ∉ b }), f ↑a ∈ e

Tactic:
exact ⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩

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

Goal state before:
pp: case refine_1.negSucc
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
a✝ : ℕ
hx : Int.negSucc a✝ ∈ u
⊢ (∃ a ∈ v', ↑a = Int.negSucc a✝) ∨ ∃ a ∈ v', Int.negSucc a = Int.negSucc a✝

Tactic:
exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ tprod (f ∘ ⇑g) = ∏ b ∈ hf_fin.toFinset, f b

Tactic:
tprod_eq_prod' hfg_fin.coe_toFinset.ge,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ ∏ b ∈ hfg_fin.toFinset, (f ∘ ⇑g) b = ∏ b ∈ hf_fin.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
hb : f b = 0
s : Finset β
hs : {b} ⊆ s
⊢ 0 = ∏ b ∈ s, f b

Tactic:
exact (Finset.prod_eq_zero (Finset.singleton_subset_iff.mp hs) hb).symm

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
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
⊢ (∀ (n : ℕ), ys n ∈ f '' K) → ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)

Tactic:
ys_in_fK

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
ys_in_fK : ∀ (n : ℕ), ys n ∈ f '' K
⊢ ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
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:
simp only [ne_eq, or_false, not_true_eq_false] at hb

Goal state after:
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))
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift' gen

Tactic:
by
      rw [lift'_lift'_assoc]
      · exact monotone_id.relComp monotone_id
      · exact monotone_gen

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
⊢ ∃ a,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖(j (a 0))⁻¹ * b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos
  choose g hg using v_in
  exact
    ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀,
      fun n hn => by simpa [hg] using hv_pos n hn⟩

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: 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
x y : X
⊢ d x y = 0 ↔ Inseparable x y

Tactic:
refine Iff.trans ?_ hB.inseparable_iff_uniformity.symm

Goal state after:
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
x y : X
⊢ d x y = 0 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun x_1 ↦ edist (x_1 x) (x_1 y)

pp: case refine_2
α : Type u_4
β : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous[Pi.topologicalSpace, _] fun x_1 ↦ ↑K * edist x y

Tactic:
exacts [.edist (continuous_apply x) (continuous_apply y), continuous_const]

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

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

Tactic:
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.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
y : α
⊢ BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)

Tactic:
rcases hs with ⟨z, hz⟩
    refine ⟨f z - K * dist y z, ?_⟩
    rintro w ⟨t, rfl⟩
    dsimp
    rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
    calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left

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 y) (G n y) + dist (g y) 0 < C + 1

Tactic:
constructor <;> constructor <;> linarith

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ≥0
⊢ ∃ x, ↑r < ‖x‖ₑ

Tactic:
exact mod_cast exists_lt_nnnorm α r

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist (e.symm.toFun (e.toEquiv x)) (e.symm.toFun (e.toEquiv y)) = ↑(ratio e)⁻¹ * edist (e.toEquiv x) (e.toEquiv y)

Tactic:
simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist x y = ↑(ratio e)⁻¹ * (↑(ratio e) * edist x y)
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ a • c < b • d

Tactic:
by
  refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_
  refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_left c d (le_of_lt h₂) b) ?_
  by_contra hbdc
  have h : d ≤ c := IsOrderedCancelSMul.le_of_smul_le_smul_left b d c hbdc
  rw [@lt_iff_le_not_ge] at h₂
  simp_all only [not_true_eq_false, and_false]

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

Goal state before:
pp: 𝕜 : Type u_4
h : NormedField 𝕜
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // h'.toNormedField = h }

Tactic:
by
  by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
  · exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩
  · simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
             sub_zero]
    refine Or.inl ⟨1, zero_lt_one, ?_⟩
    contrapose! H
    refine H.imp ?_
    -- contextual to reuse the `a ≠ 0` hypothesis in the proof of `a ≠ 0 ∧ ‖a‖ ≠ 1`
    simp +contextual [ne_of_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
⊢ Measurable f

Tactic:
nontriviality β

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
⊢ Measurable f
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case inl
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hjn : j ≤ n
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

pp: case inr
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
· exact Or.inl (h' hjn hj)

Goal state after:
case inr
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet {x}

Tactic:
← ofPred_eq_eq_singleton,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableEq α
⊢ ∀ (x : α), MeasurableSet {n | n = x}
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· exact False.elim (lt_asymm h h')

Goal state after:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : 0 < a
⊢ False

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

pp: case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

pp: case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0

Tactic:
· exact False.elim (lt_asymm h h')

Goal state after:
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1

case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1

case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ ∑' (b : { x // x ∉ x✝ }), (fun i ↦ ↑(f i)) ↑b = ↑(∑' (b : { x // x ∉ x✝ }), f ↑b)

Tactic:
ENNReal.coe_tsum

Goal state after:
case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ ∑' (b : { x // x ∉ x✝ }), (fun i ↦ ↑(f i)) ↑b = ∑' (a : { x // x ∉ x✝ }), ↑(f ↑a)

case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ Summable fun b ↦ f ↑b
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x b ↦ b ∈ f x) x' b

Tactic:
have hopen : IsOpen {x' : α | b ∈ f x'} := by
    simpa using h.preimage (continuous_id.prodMk continuous_const)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
hopen : IsOpen[inst✝¹] {x' | b ∈ f x'}
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x b ↦ b ∈ f x) x' b
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun n ↦ (f n).toNNReal

Tactic:
apply NNReal.summable_coe.1

Goal state after:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun a ↦ ↑(f a).toNNReal
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
⊢ ∑' (x : α), 1 = ↑(ENat.card α)

Tactic:
rw [← tsum_univ]

Goal state after:
α : Type u_4
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : α), c = ↑(ENat.card α) * c

Tactic:
rw [← tsum_univ]

Goal state after:
α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : a < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
obtain ⟨a', aa', a0'⟩ := exists_between a0

Goal state after:
case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : a * ⊤ < c
b0 : 0 < ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c