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

Goal state before:
pp: n : ℕ
p : ℝ
hn : n ≠ 0
⊢ ↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p

Tactic:
by
  simp only [← not_lt, ofReal_lt_natCast hn]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
y : α
hy : y ∈ s.ordConnectedSection
x : ↑s
h : [[s.ordConnectedProj x, y]] ⊆ s
⊢ s.ordConnectedProj x = y

Tactic:
rcases hy with ⟨y, rfl⟩

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
  · rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]
    exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
  simp_rw [not_exists, not_lt] at h
  refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENNReal.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_
  rw [← sub_sub_cancel ha (h _)]
  exact tsub_le_tsub_left (iInf_le (a - f ·) i) _

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

Goal state before:
pp: m n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]

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

Goal state before:
pp: ⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1

Tactic:
← ENNReal.mul_inv_cancel three_ne_zero ofNat_ne_top

Goal state after:
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 3 * 3⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
    simp only [zpow_negSucc, coe_inv this, coe_pow]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall x ε

Tactic:
mem_closedEBall,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ edist x x ≤ ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
simp only [PseudoMetricSpace.uniformity_dist, dist_nndist, edist_nndist,
    Metric.uniformity_edist_aux]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
a : α
⊢ a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : y ∈ closedEBall x ε
⊢ y ∈ UniformSpace.ball x {p | edist p.1 p.2 ≤ ε}

Tactic:
mem_closedEBall,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : edist y x ≤ ε
⊢ y ∈ UniformSpace.ball x {p | edist p.1 p.2 ≤ ε}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hx : ¬IsMax x
⊢ (u ∩ Ioi x).Nonempty

Tactic:
by
  by_contra h
  exact hx (IsMax.of_disjoint_nhds_Ioi hu (Set.disjoint_iff_inter_eq_empty.mpr
    (Set.not_nonempty_iff_eq_empty.mp h)))

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

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
let := h.resolve_left (lt_irrefl _)

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: case inr
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
h✝ : Nonempty F
y : ι
h : (fun x ↦ ‖g x‖) (f y) = ‖g‖
⊢ ‖g‖ ≤ ‖g ∘ f‖

Tactic:
exact h ▸ norm_le_pi_norm' (g ∘ f) y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
⊢ f (⨅ i, g i) = ⨅ i, f (g i)

Tactic:
iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
⊢ f (sInf (range fun i ↦ g i)) = ⨅ i, f (g i)
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
⊢ sInf (range (f ∘ g)) = ⨅ i, f (g i)

Tactic:
iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
⊢ sInf (range (f ∘ g)) = sInf (range fun i ↦ f (g i))
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
⊢ f (⨅ i, g i) = ⨆ i, f (g i)

Tactic:
iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
⊢ f (sInf (range fun i ↦ g i)) = ⨆ i, f (g i)
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
⊢ sInf (range (f ∘ g)) = ⨅ i, f (g i)

Tactic:
iInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
⊢ sInf (range (f ∘ g)) = sInf (range fun i ↦ f (g i))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous[inst✝³, inst✝⁴] f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
rw [mem_lowerBounds, forall_mem_range] at hx

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous[inst✝³, inst✝⁴] f
h : HasCompactMulSupport f
x : β
hx : ∀ (i : β), f x ≤ f i
⊢ ∃ x, ∀ (y : β), f x ≤ f y
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case inr.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
· calc
      edist a b ≤ ediam t := edist_le_ediam_of_mem h'a h'b
      _ ≤ ediam s + edist x y + ediam t := le_add_self

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing (map (algebraMap S R) p) =
    ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset
    (s := {v | v.asIdeal ∣ p.map (algebraMap S R)}.toFinset), ← Finset.prod_set_coe,
    ← Finset.prod_set_coe]

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ i, (↑i).maxPowDividing (map (algebraMap S R) p) = ∏ i, ↑i ^ (↑i).ramificationIdx S

case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ (mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)) ⊆ ↑{v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset
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 : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
⊢ Ioi (f a) ⊆ f '' Ioi a

Tactic:
by
  intro y hy
  have := intermediate_value_Ici hf htop (mem_Ici_of_Ioi hy)
  grind

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

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atBot

Tactic:
simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)

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

Goal state before:
pp: x y : ℕ
⊢ dist ↑x ↑y = dist x y

Tactic:
by
  rw [← Nat.dist_cast_real, ← Rat.dist_cast]; congr

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

Goal state before:
pp: ⊢ Pairwise fun x y ↦ 1 ≤ dist ↑x ↑y

Tactic:
by simpa using Nat.pairwise_one_le_dist

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

Goal state before:
pp: case cons
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (∏ i ∈ Finset.cons i s hi, f i)⁻¹ = ∏ i ∈ Finset.cons i s hi, (f i)⁻¹

Tactic:
| cons i s hi ih =>

Goal state after:
case cons
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (∏ i ∈ Finset.cons i s hi, f i)⁻¹ = ∏ i ∈ Finset.cons i s hi, (f i)⁻¹
Module: Mathlib.Data.EReal.Operations

Goal state before:

Tactic:
(x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := by gcongr

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
⊢ Tendsto u f (𝓝 (limsup u f))

Tactic:
apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
⊢ limsup u f ≤ liminf u f
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
⊢ (a, b) ∈ (s ∩ Metric.eball x ↑δ) ×ˢ (t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}) →
    f (a, b) ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ f (a, b) ∈ Metric.closedEBall (f (x, y)) ε
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
l : Filter β
b : ι → Set β
hl : l.HasBasis (fun x ↦ True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Tactic:
obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
  exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩

Goal state after:
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
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f

Tactic:
exact y_z.trans_le (le_limsup_of_frequently_le (h z z_x) 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:
rw [map_atTop_eq, atTop]
  refine Function.Surjective.iInf_congr Finset.card Finset.exists_card_eq fun s ↦ congr(𝓟 $(?_))
  ext
  refine ⟨Infinite.exists_superset_card_eq _ _, ?_⟩
  aesop (add safe apply Finset.card_le_card)

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 : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1 ∘ g) a ↔ HasProd f a

pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1

Tactic:
extend_comp hg

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd f a ↔ HasProd f a

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by_cases hf : f.mulSupport.Finite

Goal state after:
case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : (mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂

case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case e'_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ s₁ ⊔ s₂ = ⨆ b, bif b then s₁ else s₂

pp: case e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)

Tactic:
· simp only [iSup_bool_eq, cond]

Goal state after:
case e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1

Tactic:
← hasProd_one_iff,

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ HasProd f 1
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
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 ↦ update f b x b_1 * if b_1 = b then f b else 1) (a * x) L
⊢ a * x = a' * f b

Tactic:
exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b) L))

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

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
by
  simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
  exact hf.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg hfg

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Metric.ediam univ = Metric.ediam univ

Tactic:
← h.range_eq_univ,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Metric.ediam univ = Metric.ediam (range ⇑h)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
⊢ SequentialSpace X

Tactic:
let : TopologicalSpace X := ⨆ i, t i

Goal state after:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ i, t i
⊢ SequentialSpace X
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
refine ⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩
  rw [← coe_comp_toNNReal_comp hf]
  exact (tendsto_coe_toNNReal ha).comp h

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a

Tactic:
by
  rw [extend, if_pos hf]
  exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

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

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

Tactic:
by
    have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl
    have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl
    rw [hmn, hnm, map_comp, map_comp]
    · exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))
    repeat' exact uniformContinuous_const_smul _

Goal state after: