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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : Icc x y ⊆ Icc s t
⊢ f x < f y

Tactic:
replace : StrictMonoOn f (Icc x y) := StrictMonoOn.mono hf_mono_st this

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t)
hsx : s ≤ x
hyt : y ≤ t
this : StrictMonoOn f (Icc x y)
⊢ f x < f y
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : Dense ↑s
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)

Tactic:
simp only [hd, xor_true]
    rintro ⟨a, rfl⟩
    exact not_denseRange_zpow hd

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b

Tactic:
exact (h_mono hx hcs hxc.le).trans_lt hcb

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop f
⊢ BddAbove (range f)

Tactic:
rw [← Nat.cofinite_eq_atTop] at hf
  exact hf.bddAbove_range_of_cofinite

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

Goal state before:
pp: case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

Tactic:
obtain rfl := htop rfl rfl

Goal state after:
case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
⊢ 0 < -a ↔ a < 0

Tactic:
rw [lt_neg_comm, neg_zero]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: β : Type u_2
α : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
f : Filter α
inst✝ : f.NeBot
b : β
⊢ limsup (fun x ↦ b) f = b

Tactic:
by
  simpa only [limsup_eq, eventually_const] using! csInf_Ici

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

Goal state before:
pp: ι : Type x
α : ι → Type u
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : Fintype ι
i : ι
f g : (x : ι) → α x
⊢ edist (eval i f) (eval i g) ≤ edist f g

Tactic:
by convert! edist_le_pi_edist f g i

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

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

Tactic:
cases a <;> norm_cast

Goal state after:
case coe
b a✝ : ℝ
⊢ a✝ + b - b = a✝
Module: Mathlib.Data.EReal.Operations

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

Tactic:
cases a <;> norm_cast

Goal state after:
case coe
b a✝ : ℝ
⊢ b - (a✝ + b) = -a✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ x < ⊤

Tactic:
exact hx_top.lt_top

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

Goal state before:
pp: case pos
α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝ : Nonempty α
h : IsDirectedOrder α
s : Finset α
a : α
ha : ∀ i ∈ s, i ≤ a
⊢ ∃ i, ∀ (a : α), i ≤ a → s ⊆ Finset.Iic a

Tactic:
exact ⟨a, fun b hb c hc ↦ by simpa using (ha c hc).trans hb⟩

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

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

Tactic:
or_iff_not_imp_left

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
⊢ (¬∀ᶠ (s : Finset β) in L.filter, b ∈ s) → ∀ᶠ (s : Finset β) in L.filter, b ∉ s
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
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht : t ∈ ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s}
⊢ ↑t ⊆ L.support → ∏ b ∈ t, f b = ∏ b ∈ (↑s ∩ L.support).toFinset, f b

Tactic:
ht'

Goal state after:
α : 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
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht : t ∈ ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s}
ht' : ↑t ⊆ L.support
⊢ ∏ b ∈ t, f b = ∏ b ∈ (↑s ∩ L.support).toFinset, f b
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
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht : t ∈ ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s}
ht' : ↑t ⊆ L.support
⊢ ∏ b ∈ t, f b = ∏ b ∈ (↑s ∩ L.support).toFinset, f b

Tactic:
simp only [Set.mem_iInter] at ht

Goal state after:
α : 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
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∏ b ∈ t, f b = ∏ b ∈ (↑s ∩ L.support).toFinset, f b
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
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
classical
  let : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  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: β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ (Multipliable fun x ↦ a) ↔ a = 1

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · by_contra ha
    have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
    have : Finite β := by
      simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
    exact not_finite β
  · rintro rfl
    exact multipliable_one

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

Goal state before:

Tactic:
(∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

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

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

Tactic:
by
  rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
  conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
  exact h.sigma' fun n ↦ (hasSum_fintype _).summable

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
inst✝ : Fintype α
g : β → γ
hg : Isometry g
x✝¹ x✝ : α → β
⊢ edist ((fun f ↦ g ∘ f) x✝¹) ((fun f ↦ g ∘ f) x✝) = edist x✝¹ x✝

Tactic:
simp [edist_pi_def, hg.edist_eq]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
m n : ℕ
x x2 : Fin m → α
y y2 : Fin n → α
⊢ edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)

Tactic:
by
  simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv),
    iSup_sum]

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

Goal state before:
pp: case inl
xt : 0 ≠ ∞
⊢ (𝓝 ⊥).HasBasis (fun x ↦ x ≠ ⊥) fun ε ↦ Icc ⊥ ε

Tactic:
Icc_bot,

Goal state after:
case inl
xt : 0 ≠ ∞
⊢ (𝓝 ⊥).HasBasis (fun x ↦ x ≠ ⊥) fun ε ↦ Iic ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case pos
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ε = ∞
⊢ min 1 (ε / 2) < ε

pp: case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ min 1 (ε / 2) < ε

Tactic:
· simp [hε_top]

Goal state after:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ min 1 (ε / 2) < ε
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:
induction s using Finset.induction with

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

Goal state before:
pp: case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (extend f)

Tactic:
rw [extend, if_pos hf]
    exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf

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

Goal state before:
pp: case e'_4
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'✝ : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = drop (M + 1) L

Tactic:
drop_zipWith,

Goal state after:
case e'_4
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
hMs'✝ : (drop (M + 1) L).sum ≤ (take (M + 1) L).sum
hMs' : 2 * (drop (M + 1) L).sum ≤ L.sum
⊢ zipWith d (drop M l) (drop (M + 1) l ++ [y]) = zipWith d (drop (M + 1) (x :: l)) (drop (M + 1) (l ++ [y]))
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case neg
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
h : ¬∃ n, (x, y) ∉ U n
⊢ 0 = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff] using h

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

Goal state before:
pp: a b : ℝ
h : a ≤ b
⊢ Metric.diam (Icc a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

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

Goal state before:
pp: a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ico a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

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

Goal state before:
pp: a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioc a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

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

Goal state before:
pp: a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioo a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
by
  refine le_mul_of_forall_lt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
  exact (mul_lt_mul a_x b_x).trans c_ab

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this : IsClosed[instTopologicalSpaceProd] {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend f x = f ⟨x, hx⟩
⊢ (x, y) ∈ {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}

Tactic:
have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this : IsClosed[instTopologicalSpaceProd] {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend f x = f ⟨x, hx⟩
Ay : hs.extend f y = f ⟨y, hy⟩
⊢ (x, y) ∈ {p | edist (hs.extend f p.1) (hs.extend f p.2) ≤ ↑K * edist p.1 p.2}
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_2
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 : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑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
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ ↑(1 / 2) ^ (n + 1) ≤ ↑(d x.1 x.2) / 2

Tactic:
rwa [← NNReal.coe_two, ← NNReal.coe_div, ← NNReal.coe_pow, NNReal.coe_le_coe, pow_succ,
      mul_one_div, div_le_iff₀ zero_lt_two, div_mul_cancel₀ _ two_ne_zero, hle_d]

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

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

Tactic:
· rw [inf_comm c, inf_comm c]
        exact abs_inf_sub_inf_le_abs _ _ _

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

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' eball b r = eball (b / a) r

Tactic:
div_eq_mul_inv

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' eball b r = eball (b * a⁻¹) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b / a) r

Tactic:
div_eq_mul_inv

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b * a⁻¹) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
div_eq_mul_inv

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Tactic:
div_eq_mul_inv

Goal state after:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : Preorder 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:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_left c d h₂ a) ?_
  refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_right a b (le_of_lt h₁) d) ?_
  by_contra hbad
  have h : b ≤ a := IsOrderedCancelSMul.le_of_smul_le_smul_right b a d hbad
  rw [@lt_iff_le_not_ge] at h₁
  simp_all only [not_true_eq_false, and_false]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(a :: b :: l).prod‖ ≤ (‖a‖ :: map norm (b :: l)).prod

Tactic:
List.prod_cons,

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * (b :: l).prod‖ ≤ (‖a‖ :: map norm (b :: l)).prod
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

Tactic:
rcases s with ⟨⟨l⟩, hl⟩
  simpa using! (l.map f).norm_prod_le

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

Goal state before:
pp: 𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
h : BddAbove (Set.range fun k ↦ ‖k‖)
⊢ False

Tactic:
obtain ⟨x, h⟩ := h

Goal state after:
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k ↦ ‖k‖)
⊢ False
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Tactic:
by
  refine ⟨?_, continuousAt_zpow₀ _ _⟩
  contrapose!
  rintro ⟨rfl, hm⟩ hc
  exact (hc.tendsto.mono_left nhdsWithin_le_nhds).not_tendsto (Metric.disjoint_nhds_cobounded _)
    (tendsto_zpow_nhdsNE_zero_cobounded hm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
refine ⟨fun hst => ?_, fun h => h.1.prod h.2⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ¬zero ≤ neg

Tactic:
rintro ⟨_⟩

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

Goal state before:
pp: ⊢ ¬pos ≤ zero

Tactic:
rintro ⟨_⟩

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

Goal state before:
pp: ⊢ ¬pos ≤ neg

Tactic:
rintro ⟨_⟩

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
rintro ⟨_⟩

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

Goal state before:
pp: a : SignType
ha : a ≠ 0
⊢ a * id a = 1

Tactic:
by cases a <;> trivial

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

Goal state before:
pp: ⊢ ∀ (x : SignType), - -x = x

Tactic:
rintro ⟨_⟩

Goal state after:
case zero
⊢ - -zero = zero

case neg
⊢ - -neg = neg

case pos
⊢ - -pos = pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢

Goal state after:
case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ 0 < ∑ i ∈ s, f i
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ (algebraMap R A) r ∈ closure[inst✝⁵] ↑s

Tactic:
apply subset_closure

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
A : Type u_2
inst✝⁶ : Semiring A
inst✝⁵ : TopologicalSpace A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : TopologicalSpace B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ (algebraMap R A) r ∈ ↑s