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

Goal state before:
pp: 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'
A : u ⊆ u1 ∪ u2
⊢ ((∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x

Tactic:
]

Goal state after:
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'
A : u ⊆ u1 ∪ u2
⊢ ((∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) = (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∏' (b : ↑s), ?m.37 b = ∏' (x : ↑s), s.mulIndicator f ↑x

pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = ?m.37 b

pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ↑s → α

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = s.mulIndicator f ↑b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / f 0)
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)

Tactic:
]

Goal state after:
G : Type u_2
inst✝² : CommGroup G
g g' : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun n ↦ f ↑n) g
hf₂ : HasProd (fun n ↦ f (-↑(n + 1))) (g' / f 0)
⊢ HasProd (fun n ↦ f (-(↑n + 1))) (g' / f 0)
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 α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ ∑' (c : (n : A) × ↥(antidiagonal n)),
      f (HasAntidiagonal.sigmaAntidiagonalEquivProd c).1 * g (HasAntidiagonal.sigmaAntidiagonalEquivProd c).2 =
    ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2

Tactic:
]

Goal state after:
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ ∑' (c : (n : A) × ↥(antidiagonal n)),
      f (HasAntidiagonal.sigmaAntidiagonalEquivProd c).1 * g (HasAntidiagonal.sigmaAntidiagonalEquivProd c).2 =
    ∑' (x : A) (b : ↑↑(antidiagonal x)), f (↑b).1 * g (↑b).2
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
⊢ Multipliable f ↔ Multipliable f

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Tactic:
have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _
  simp_rw [← hg.tprod_eq this, hg.extend_apply]

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

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
⊢ Multipliable fun x ↦ f ↑x

Tactic:
]

Goal state after:
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
⊢ Multipliable fun x ↦ f ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ ∏' (x : ↑{j}), (s ↑x).mulIndicator f i = f i

pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ (mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ ∏' (x : ↑{j}), (s ↑x).mulIndicator f i = f i

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ (mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
h3 : Multipliable fun n ↦ f ↑↑n
⊢ Multipliable fun x ↦ f (-↑x)

Tactic:
]

Goal state after:
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
h3 : Multipliable fun n ↦ f ↑↑n
⊢ Multipliable fun x ↦ f (-↑x)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
⊢ 1 + a = x

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
⊢ 1 + a = x
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: x : ℝ≥0
⊢ 𝓝[toReal '' Set.Ioi x] ↑x = 𝓝[>] ↑x

Tactic:
image_coe_Ioi

Goal state after:
x : ℝ≥0
⊢ 𝓝[>] ↑x = 𝓝[>] ↑x
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: x : ℝ≥0
⊢ 𝓝[>] ↑x = 𝓝[>] ↑x

Tactic:
]

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

Goal state before:
pp: x : ℝ≥0
⊢ 𝓝[≥] ↑x = 𝓝[≥] ↑x

Tactic:
]

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

Goal state before:
pp: ⊢ atTop = atTop

Tactic:
]

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

Goal state before:
pp: α : Type u_2
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto (fun x ↦ (f x).toNNReal) l atTop

Tactic:
]

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

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc x' y'

Tactic:
]

Goal state after:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc x' y'
Module: Mathlib.Topology.MetricSpace.Pseudo.Real

Goal state before:
pp: x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc x' y'

Tactic:
]

Goal state after:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc x' y'
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable fun a ↦ ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a ↦ ↑((f ∘ i) a)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable fun a ↦ ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a ↦ ↑((f ∘ i) a)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a ↦ ↑(f (a + k))) ↔ Summable fun a ↦ ↑(f a)

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a ↦ ↑(f (a + k))) ↔ Summable fun a ↦ ↑(f a)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
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:
simp_rw [← neg_mul] at hsum'

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 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ ↑K * ediam s ≤ ↑K * ediam s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ ↑K * edist x y
⊢ edist (g x) (g y) ≤ ↑K * edist x y

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ ↑K * edist x y
⊢ edist (g x) (g y) ≤ ↑K * edist x y
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}
⊢ ↑K * edist (f x.1) (f x.2) < ε

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}
⊢ ↑K * edist (f x.1) (f x.2) < ε
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}
⊢ edist (f x.1) (f x.2) * ↑K < ε

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}
⊢ edist (f x.1) (f x.2) * ↑K < ε
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: β : Type u_2
inst✝² : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst✝¹ : EMetricSpace α
inst✝ : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K = 0
⊢ K = 0

Tactic:
]

Goal state after:
β : Type u_2
inst✝² : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst✝¹ : EMetricSpace α
inst✝ : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K = 0
⊢ K = 0
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:
]

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) '' s)
⊢ Bornology.IsBounded s
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 : X
l : List X
⊢ (zipWith d (y :: l.reverse).reverse (x :: l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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 : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
reverse_cons,

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 : X
l : List X
⊢ (zipWith d (l.reverse.reverse ++ [y]) (x :: l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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 : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length
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 : X
l : List X
⊢ (zipWith d (x :: l) (l ++ [y])).sum = (zipWith d (x :: l) (l ++ [y])).sum

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 : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
]

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 : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length
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
⊢ ⨅ l, (zipWith d (x :: l) (l ++ [z])).sum ≤
    (⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ⨅ l, (zipWith d (y :: l) (l ++ [z])).sum

Tactic:
]

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
⊢ ⨅ l, (zipWith d (x :: l) (l ++ [z])).sum ≤
    (⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ⨅ l, (zipWith d (y :: l) (l ++ [z])).sum
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]) ++ zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
← zipWith_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 ++ y :: lyz) (lxy ++ [y] ++ (lyz ++ [z]))).sum

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
⊢ (x :: lxy).length = (lxy ++ [y]).length
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 ++ ([y] ++ lyz))) (lxy ++ ([y] ++ (lyz ++ [z])))).sum

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
⊢ (x :: lxy).length = (lxy ++ [y]).length

Tactic:
]

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
⊢ (x :: lxy).length = (lxy ++ [y]).length
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ (Finset.univ.sup fun b ↦ edist (Pi.single i x b) (Pi.single i y b)) = edist x y

Tactic:
]

Goal state after:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ (Finset.univ.sup fun b ↦ edist (Pi.single i x b) (Pi.single i y b)) = edist x y
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
⊢ lxy.length + 1 = lxy.length + 1

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : α
⊢ max (edist ((AddMonoidHom.inl α β) x).1 ((AddMonoidHom.inl α β) y).1)
      (edist ((AddMonoidHom.inl α β) x).2 ((AddMonoidHom.inl α β) y).2) =
    edist x y

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : α
⊢ max (edist ((AddMonoidHom.inl α β) x).1 ((AddMonoidHom.inl α β) y).1)
      (edist ((AddMonoidHom.inl α β) x).2 ((AddMonoidHom.inl α β) y).2) =
    edist x y
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : β
⊢ max (edist ((AddMonoidHom.inr α β) x).1 ((AddMonoidHom.inr α β) y).1)
      (edist ((AddMonoidHom.inr α β) x).2 ((AddMonoidHom.inr α β) y).2) =
    edist x y

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : β
⊢ max (edist ((AddMonoidHom.inr α β) x).1 ((AddMonoidHom.inr α β) y).1)
      (edist ((AddMonoidHom.inr α β) x).2 ((AddMonoidHom.inr α β) y).2) =
    edist x y
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist x y = edist x y

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (f '' univ) = Metric.ediam univ

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (f '' univ) = Metric.ediam univ
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ (Metric.ediam s).toReal = (Metric.ediam s).toReal

Tactic:
]

Goal state after: