mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case codisjoint.ofNat
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
i : ℕ
⊢ Int.ofNat i ∈ ⊤ → Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

pp: case codisjoint.negSucc
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
j : ℕ
⊢ Int.negSucc j ∈ ⊤ → Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
<;>

Goal state after:
case codisjoint.ofNat
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
i : ℕ
⊢ Int.ofNat i ∈ ⊤ → Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

case codisjoint.negSucc
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
j : ℕ
⊢ Int.negSucc j ∈ ⊤ → Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ (∃ a ∈ v', ↑a = x) ∨ ∃ a ∈ v', -↑a = x

Tactic:
refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [Int.natCast_natAbs, abs_eq_self, h'x]

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f ↑n

pp: case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f (-(↑n + 1))

Tactic:
<;>

Goal state after:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f ↑n

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f (-(↑n + 1))
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f ↑n

pp: case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f (-↑n)

Tactic:
<;>

Goal state after:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f ↑n

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable fun n ↦ f (-↑n)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
hP : P
⊢ (∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
hP : ¬P
⊢ (∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
hP : P
⊢ (∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h

case neg
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
hP : ¬P
⊢ (∏'[L] (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏'[L] (b : β), x b h
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → P → α
hP : P
⊢ (∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → P → α
hP : ¬P
⊢ (∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → P → α
hP : P
⊢ (∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1

case neg
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
P : Prop
inst✝ : Decidable P
x : β → P → α
hP : ¬P
⊢ (∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : n = b
⊢ f n = f n * update f b 1 n

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : ¬n = b
⊢ f n = 1 * update f b 1 n

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : n = b
⊢ f n = f n * update f b 1 n

case neg
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : ¬n = b
⊢ f n = 1 * update f b 1 n
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ uIcc (x' b) (y' b)

pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ uIcc (x' b) (y' b)

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ uIcc (x' b) (y' b)

case refine_2
ι : Type u_1
inst✝ : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ uIcc (x' b) (y' b)
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 * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)

Tactic:
← tsum_neg,

Goal state after:
ι : 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 * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + ∑' (b : ι), -(f b * ∏ i < b, (1 + -f i))
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case succ.none
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ none ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr none

pp: case succ.some
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
val✝ : NNReal
⊢ some val✝ ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr (some val✝)

Tactic:
<;>

Goal state after:
case succ.none
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ none ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr none

case succ.some
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
val✝ : NNReal
⊢ some val✝ ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr (some val✝)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded ((fun a ↦ f a b) '' s)
⊢ Bornology.IsBounded s

Tactic:
replace h := (hf b).isBounded_preimage h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded ((fun a ↦ f a b) ⁻¹' (fun a ↦ f a b) '' s)
⊢ Bornology.IsBounded s
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
have := hl.1

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, l ≤ 𝓝 x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
⊢ ↑{a | a < ∞} ≃ₜ ℝ≥0

Tactic:
refine (Homeomorph.setCongr ?_).trans neTopHomeomorphNNReal
  simp only [lt_top_iff_ne_top]

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

Goal state before:
pp: case refine_1
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u

Tactic:
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
    refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H 1 ((f x.fst.fst x.snd)⁻¹ * f x.fst.snd x.snd) ?_
    simpa [dist_eq_norm_inv_mul, norm_div_rev] using hx

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

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

pp: case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥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
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_2.zero
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ v 0 ∈ s

Tactic:
change w 0 ∈ s

Goal state after:
case refine_2.zero
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ w 0 ∈ s
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case succ.refine_1
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

pp: case succ.refine_2
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

Tactic:
<;>

Goal state after:
case succ.refine_1
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

case succ.refine_2
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
⊢ x ≠ 0 ∨ x ^ n ≠ ∞
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case mp
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) → Nonempty α

pp: case mpr
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty α → Nonempty (CauchyFilter α)

Tactic:
<;>

Goal state after:
case mp
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) → Nonempty α

case mpr
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty α → Nonempty (CauchyFilter α)
Module: Mathlib.Topology.UniformSpace.Completion

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

Tactic:
by_cases hf : UniformContinuous f
  · rw [extend, if_pos hf]
    exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf
  · rw [extend, if_neg hf]
    exact uniformContinuous_of_const fun a _b => by congr

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

Goal state before:
pp: α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ a ≠ 0 ∨ b⁻¹ ≠ ∞

pp: α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞

Tactic:
<;>

Goal state after:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ a ≠ 0 ∨ b⁻¹ ≠ ∞

α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + ε

pp: case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + ε

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + ε

case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + ε
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + C * ↑δ

pp: case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + C * ↑δ

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f y + C * edist x y ≤ f y + C * ↑δ

case refine_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * ↑δ < ε
y : α
hy : y ∈ closedEBall x ↑δ
⊢ f x + C * edist y x ≤ f x + C * ↑δ
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' ≤ edist (x, y) (x', y')

pp: case h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist y y' ≤ edist (x, y) (x', y')

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' ≤ edist (x, y) (x', y')

case h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist y y' ≤ edist (x, y) (x', y')
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
⊢ min t x ≠ ∞

Tactic:
simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Tactic:
by
  rw [iterate_succ, mul_comm]
  simpa only [NNReal.coe_pow] using! (hf.iterate n).dist_le_mul x (f x)

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

Goal state before:
pp: ⊢ LipschitzWith 1 Real.toNNReal

Tactic:
refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)
  simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using!
    lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)

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

Goal state before:
pp: case refine_1
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 : ℕ
hn : True
x : X × X
hx : x ∈ U n
⊢ ¬(x.1, x.2) ∉ U n

Tactic:
Classical.not_not

Goal state after:
case refine_1
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 : ℕ
hn : True
x : X × X
hx : x ∈ U n
⊢ (x.1, x.2) ∈ U n
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ ∀ x ∈ univ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[univ] x) fun y ↦ dist (f y) 0

pp: case hg
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ ∀ x ∈ univ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[univ] x) fun y ↦ dist (g y) 0

Tactic:
<;>

Goal state after:
case hf
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ ∀ x ∈ univ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[univ] x) fun y ↦ dist (f y) 0

case hg
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ ∀ x ∈ univ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[univ] x) fun y ↦ dist (g y) 0
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 → x ≠ 0

pp: case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ x ≠ 0 → ‖x‖ = 1

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 → x ≠ 0

case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ x ≠ 0 → ‖x‖ = 1