mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 < r
⊢ dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr.le
  simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N^[x✝ + 1] 0)

Tactic:
iterate_succ_apply'

Goal state after:
case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N (N^[x✝] 0))
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N^[x✝ + 1] 0

Tactic:
iterate_succ_apply'

Goal state after:
case refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: β : Type v
γ : Type w
inst✝¹ : MetricSpace γ
inst✝ : PseudoMetricSpace β
f : γ → β
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
s : Set γ
ε : ℝ
hε : 0 < ε
hs : s.Pairwise fun x y ↦ ε ≤ dist x y
⊢ s.Pairwise fun x y ↦ (x, y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
by simpa using hs

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

Goal state before:
pp: α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
u : ℕ → α
hu : Monotone u ∧ (∀ (n : ℕ), u n ≤ sSup S) ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
exact ⟨u, hu.1, hu.2.2⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (c.divMod b a) * b = c

Tactic:
rw [divMod, dif_pos ⟨hac, ha, hb⟩]
  exact (IsDedekindDomain.exists_add_spanSingleton_mul_eq hac ha hb).choose_spec

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
⊢ Continuous[inst✝, inst✝³] fun x ↦ sSup (f x '' K)

Tactic:
by
  rcases eq_empty_or_nonempty K with (rfl | h0K)
  · simp_rw [image_empty]
    exact continuous_const
  rw [continuous_iff_continuousAt]
  intro x
  obtain ⟨y, hyK, h2y, hy⟩ :=
    hK.exists_sSup_image_eq_and_ge h0K
      (show Continuous (f x) from hf.comp <| .prodMk_right x).continuousOn
  rw [ContinuousAt, h2y, tendsto_order]
  have := tendsto_order.mp ((show Continuous fun x => f x y
    from hf.comp <| .prodMk_left _).tendsto x)
  refine ⟨fun z hz => ?_, fun z hz => ?_⟩
  · refine (this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK
    exact hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn
  · have h : ({x} : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z := by
      rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
      exact (hy y' hy').trans_lt hz
    obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ :=
      generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h
    refine eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => ?_
    rw [hK.sSup_lt_iff_of_continuous h0K
        (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn]
    exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))

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

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
ε

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
⊢ ε > 0 → ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
⊢ False

Tactic:
· by_cases! hb : f ⊥ < f b
    · obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩
      rw [hf_i hu.2] at hu
      exact (hab.trans hu.1.2).false
    · replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
      obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩
      have : u = ⊥ := hf_i hu.2
      simp_all

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (max (edist x y) (edist x z)).toReal (edist y z).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal

pp: case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

pp: case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞

Tactic:
ENNReal.toReal_max

Goal state after:
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal

case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x y ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist x z ≠ ∞

case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ IsCompact {a | f a ≤ f x₀}

Tactic:
exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h

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

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
constructor <;> intro h
  · exact h.comp hg
  · rcases tendsto_atTop_of_monotone hf with (h' | ⟨l', hl'⟩)
    · exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
    · rwa [tendsto_nhds_unique h (hl'.comp hg)]

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

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range fun i ↦ (I ∘ ⇑e) i)) = ⨅ i, emultiplicity p.asIdeal ((I ∘ ⇑e) i)
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
← sInf_range

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun i ↦ (I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ liminf s cofinite = {x | {n | x ∉ s n}.Finite}

Tactic:
by
  simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
this : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
⊢ x ∈ (fun i ↦ ⋃ b ∈ decode₂ β i, f b) i → x ∉ (fun i ↦ ⋃ b ∈ decode₂ β i, f b) j

Tactic:
by simpa [decode₂_eq_some]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ Filter.map (fun s ↦ ∏ i ∈ s, f (g i)) atTop = Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop

Tactic:
apply le_antisymm <;> refine map_atTop_finsetProd_le_of_prod_eq fun s => ?_

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)

case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', 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:
by
  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.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
⊢ ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1

Tactic:
intro b'

Goal state after:
β : 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
b' : β
⊢ (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ (b' : β), b' ≠ b → (if b' = b then a b' else 1) = 1

Tactic:
intro b'

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
⊢ b' ≠ b → (if b' = b then a b' else 1) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ (b' : β), b' ≠ b → (if b = b' then a b' else 1) = 1

Tactic:
intro b'

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
⊢ b' ≠ b → (if b = b' then a b' else 1) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 - f j)
hprod : Multipliable fun x ↦ 1 - f x
⊢ ∏' (i : ι), (1 - f i) = 1 - ∑' (i : ι), f i * ∏ j < i, (1 - f j)

Tactic:
by
  simp_rw [sub_eq_add_neg] at hsum hprod ⊢
  obtain hsum' := hsum.neg
  simp_rw [← neg_mul] at hsum'
  simp_rw [← tsum_neg, ← neg_mul]
  exact tprod_one_add_ordered hsum' hprod

Goal state after:
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 x) r

Tactic:
by
  rw [← h.preimage_symm, h.symm.preimage_closedEBall, symm_symm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ ∀ (b' : β), b' ≠ b → Pi.mulSingle b a b' = 1

Tactic:
intro b'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
b' : β
⊢ b' ≠ b → Pi.mulSingle b a b' = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this : Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ bs, f p) atTop (𝓝 (∏ b ∈ bs, g b))
⊢ ∏ b ∈ bs, g b ∈ id s

Tactic:
refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)

Goal state after:
case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image Sigma.fst u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this : Tendsto (fun t ↦ ∏ p ∈ t with p.fst ∈ bs, f p) atTop (𝓝 (∏ b ∈ bs, g b))
t : Finset ((b : β) × γ b)
ht : u ⊆ t
x : (b : β) × γ b
hx : x ∈ u
⊢ x ∈ {p ∈ t | p.fst ∈ bs}
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
⊢ a - f n ≤ ε

Tactic:
have hN_left := hn.1

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
⊢ a - f n ≤ ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
ε

Goal state after:
case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
⊢ 0 < ε → ∃ n, f n < ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
ε

Goal state after:
case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
⊢ 0 < ε → ∃ n, f n ≤ ε
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

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

Tactic:
rw [pkg.extend_def hf]

Goal state after:
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

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

Tactic:
rw [pkg.extend_def hf]

Goal state after:
case pos
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)
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
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
n : ℕ
hn : 0 < n
⊢ ‖j (g n)‖ < f n

Tactic:
simpa [hg] using hv_pos n hn

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

Goal state before:
pp: L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (s.sup f) l (𝓝 (s.sup g))

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne
  · simpa using! tendsto_const_nhds
  · simp only [← sup'_eq_sup hne]
    exact finset_sup'_nhds hne hs

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
f : E → F
C : ℝ≥0
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖

Tactic:
simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_inv_mul]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i ↦ f i / a

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup' hs f / a = s.sup fun i ↦ f i / a
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup' hs f / a = s.sup fun i ↦ f i / a

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup' hs f / a = s.sup' hs fun i ↦ f i / a
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑1 * edist x y

pp: case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑⋯.choose * edist x y

Tactic:
· rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
    replace hr := hr x y
    rcases key x y with h | h
    · simp only [hr, h, mul_zero]
    · simp [hr, h, hne]

Goal state after:
case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist (f x) (f y) = ↑⋯.choose * edist x y
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ratio (Dilation.id α) = 1

Tactic:
by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
  · rw [ratio, if_pos h]
  · rcases h with ⟨x, y, hne⟩
    refine (ratio_unique hne.1 hne.2 ?_).symm
    simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio e.symm * ratio e = 1

Tactic:
rw [← ratio_trans, symm_trans_self, ratio_refl]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ (closedBall x (‖x‖ / 2))ᶜ ∈ 𝓝 0

Tactic:
refine Metric.isClosed_closedBall.isOpen_compl.mem_nhds ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ 0 ∈ (closedBall x (‖x‖ / 2))ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
⊢ MeasurableSpace.map g (MeasurableSpace.comap g m) = m

Tactic:
refine le_antisymm (fun S hS => ?_) le_map_comap
  rw [map_def, measurableSet_comap] at hS
  aesop

Goal state after: