mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

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

Tactic:
lift z to ℝ using ⟨hz, hbot⟩

Goal state after:
case inl.inr
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ liminf f ⊥ = ⊤

Tactic:
simp [liminf]

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:
convert! edist_le_pi_edist f g i

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

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

Tactic:
| coe b =>

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:
rw [eventually_le_const_iff_forall_gt_eventually_lt_const]
  exact fun _ hc ↦ eventually_lt_of_limsup_lt hc

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

Goal state before:
pp: x : EReal
h : x < 0
⊢ x * ⊤ = ⊥

Tactic:
exact mul_top_of_neg h

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
a : β
ha : ∀ᶠ (x : α) in f, a ≤ u x
⊢ ∃ᶠ (x : α) in f, a ≤ v x

Tactic:
exact (ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x

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

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

Tactic:
rw [x.mul_comm, x.mul_comm]

Goal state after:
x y : EReal
⊢ -y * x = -(y * x)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: c : EReal
a b : ℝ≥0∞
⊢ (↑a + ↑b) * c = ↑a * c + ↑b * c

Tactic:
cases c using recENNReal with
  | coe c => exact_mod_cast add_mul a b c
  | neg_coe c hc =>
    simp only [mul_neg, ← coe_ennreal_add, ← coe_ennreal_mul, add_mul]
    rw [coe_ennreal_add, EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)),
      sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
⊢ g (limsup u f) = limsup (fun x ↦ g (u x)) f

Tactic:
by
  refine le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) ?_
  rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]
  refine g.monotone ?_
  have hf : u = fun i => g.symm (g (u i)) := funext fun i => (g.symm_apply_apply (u i)).symm
  nth_rw 2 [hf]
  refine (OrderIso.to_galoisConnection g.symm).l_limsup_le ?_ hgu_co
  simp_rw [g.symm_apply_apply]
  exact hu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (f ∘ Subtype.val)

Tactic:
have := hs.toFinset.multipliable f
  rwa [hs.coe_toFinset] at this

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 α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L

Tactic:
simp_rw [HasProd, comp_apply, ← _root_.map_prod]
  exact hg.tendsto_nhds_iff.symm

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

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
tprod_eq_one_of_not_multipliable h,

Goal state after:
case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g 1 = ∏'[L] (i : ι), g (f i)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range encode
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun b ↦ m (s b)) 1 n

Tactic:
rw [extend_apply' _ _ _ hn]

Goal state after:
case inr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range encode
⊢ m (⨆ b ∈ decode₂ β n, s b) = 1 n
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 : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
by
  classical
  let : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
by
  by_cases hf : Summable f L
  · rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
  · simp [tsum_eq_zero_of_not_summable hf]

Goal state after:
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
lxy lyz : List X
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
← sum_append,

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
lxy lyz : List X
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y]) ++ zipWith d (y :: lyz) (lyz ++ [z])).sum
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.closedEBall x r = Metric.closedEBall (h.symm x) r

Tactic:
← h.isometry.preimage_closedEBall (h.symm x) r,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.closedEBall x r = ⇑h ⁻¹' Metric.closedEBall (h (h.symm x)) r
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
l : List X
this✝ : IsTrans X fun x y ↦ d x y = 0
this : ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
by exact this _ rfl

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

Goal state before:
pp: case h.inl
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
⊢ d x y ≤ 2 * L.sum

pp: case h.inr
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
⊢ d x y ≤ 2 * L.sum

Tactic:
· simp only [hd₀, zero_le]

Goal state after:
case h.inr
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
⊢ d x y ≤ 2 * L.sum
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
s : Set E
a : E
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a⁻¹ * b‖ < ε

Tactic:
simp [Metric.mem_closure_iff, dist_eq_norm_inv_mul]

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

Goal state before:
pp: case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩

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

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
⊢ UniformContinuous (pkg.extend f)

Tactic:
by
  by_cases hf : UniformContinuous f
  · rw [pkg.extend_def hf]
    exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf
  · unfold AbstractCompletion.extend
    rw [if_neg hf]
    exact uniformContinuous_of_const fun a b => by congr 1

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

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]
  constructor <;> intro h ε hε
  · obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨hε.ne', by finiteness⟩)⟩)
    · refine ⟨n, hn.trans_lt ?_⟩
      by_cases hε_top : ε = ∞
      · simp [hε_top]
      refine (min_le_right _ _).trans_lt ?_
      rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
      conv_lhs => rw [← mul_one ε]
      gcongr; simp
  · obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, hn.le⟩

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

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

Tactic:
| coe b =>

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

Goal state before:
pp: case refine_3.inr
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' : L.sum ≤ 2 * (take (M + 1) L).sum
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
rw [← sum_take_add_sum_drop L (M + 1), two_mul, add_le_add_iff_left, ← add_le_add_iff_right,
      sum_take_add_sum_drop, ← two_mul] at hMs'

Goal state after:
case refine_3.inr
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
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:

Tactic:
edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x ↦ min (f x) (g x)

Tactic:
simpa only [(· ∘ ·), one_mul] using! lipschitzWith_min.comp (hf.prodMk hg)

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

Goal state before:
pp: α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
    have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
    exact this.extend_real

Goal state after:
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x ↦ f x i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y

Tactic:
rcases h with ⟨r, hne, h⟩

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
Module: Mathlib.Topology.MetricSpace.Dilation

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

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

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
⊢ IsClosedEmbedding fun x_1 ↦ (Infinite.natEmbedding 𝕜) x_1 • x

Tactic:
refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (fun x_1 y ↦ ‖x‖ ≤ dist ((Infinite.natEmbedding 𝕜) x_1 • x) ((Infinite.natEmbedding 𝕜) y • x)) k n
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ c ∈ map (⇑(algebraMap 𝕜 𝕜')) (cobounded 𝕜)

Tactic:
mem_map

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ ⇑(algebraMap 𝕜 𝕜') ⁻¹' c ∈ cobounded 𝕜
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Tendsto (⇑(algebraMap 𝕜 𝕜')) (cobounded 𝕜) (cobounded 𝕜')

Tactic:
intro c hc
  rw [mem_map]
  rw [← isCobounded_def, ← isBounded_compl_iff, isBounded_iff_forall_norm_le] at hc ⊢
  obtain ⟨s, hs⟩ := hc
  exact ⟨s, fun x hx ↦ by simpa using hs (algebraMap 𝕜 𝕜' x) hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⊤ (f ⁻¹' s) = ⊤ (f '' f ⁻¹' s)

Tactic:
top_apply',

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⨅ (_ : f ⁻¹' s = ∅), 0 = ⊤ (f '' f ⁻¹' s)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⨅ (_ : f ⁻¹' s = ∅), 0 = ⊤ (f '' f ⁻¹' s)

Tactic:
top_apply',

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⨅ (_ : f ⁻¹' s = ∅), 0 = ⨅ (_ : f '' f ⁻¹' s = ∅), 0
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (restrict univ) ⊤ = ⊤

Tactic:
restrict_univ

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ ⊤ = ⊤
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < 1 / (↑n + 1)

Tactic:
one_div

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ 1 / ↑n ≤ 1

Tactic:
one_div

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ (↑n)⁻¹ ≤ 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign x) * ↑y.abs = ↑(sign y) * ↑y.abs

Tactic:
hsign

Goal state after:
case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign y) * ↑y.abs = ↑(sign y) * ↑y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ {i | ε ≤ a i}.Finite

Tactic:
by_contra h

Goal state after:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬{i | ε ≤ a i}.Finite
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ tsum (f ∘ i) ≤ tsum f

Tactic:
lift f to α → ℝ≥0 using hn

Goal state after:
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable fun i ↦ ↑(f i)
⊢ tsum ((fun i ↦ ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ c = a * b

Tactic:
rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]

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

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

Tactic:
nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' h.ne']

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ IsOpen (range Real.toEReal)

Tactic:
by simp only [range_coe_eq_Ioo, isOpen_Ioo]

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

Goal state before:
pp: case pos
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ False

pp: case neg
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ False

Tactic:
· replace h : Tendsto (fun n : ℕ ↦ |r| ^ n) atTop (𝓝 0) := by simpa only [← abs_pow, h]
      simp only [hr.symm, one_pow] at h
      exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds

Goal state after:
case neg
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ False
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
rcases t.eq_empty_or_nonempty with h | h

Goal state after:
case inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t = ∅
⊢ ⨆ (_ : t.Nonempty), m t = m t

case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
h : 0 < a
x : ℝ
⊢ ∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ↑a) ∈ t

Tactic:
use (Set.Ioi ((2 * (max (x + 1) 0) / a : ℝ) : EReal)) ×ˢ (Set.Ioi ((a / 2 : ℝ) : EReal))

Goal state after:
case h
a : ℝ
h : 0 < a
x : ℝ
⊢ (∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2) ∧
    IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)) ∧ (⊤, ↑a) ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)