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

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

Tactic:
have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
  rw [← Function.comp_def]
  by_cases hf_fin : (mulSupport f).Finite
  · have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
    lift g to γ ↪ β using hg
    simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]
    refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
    simp [this]
  · have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]
    simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : Multipliable f
⊢ ∏' (i : ι), f i ∈ s

pp: case neg
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : Multipliable f
⊢ ∏' (i : ι), f i ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case e_a.refine_1
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) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1

pp: case e_a.refine_2
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 = if x = 0 then f 0 else 1

Tactic:
·

Goal state after:
case e_a.refine_1
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) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case e_a.refine_2
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 = if x = 0 then f 0 else 1

Tactic:
·

Goal state after:
case e_a.refine_2
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 = if x = 0 then f 0 else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case he
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k) * f (2 * k)

pp: case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k + 1) * f (2 * k + 1)

Tactic:
·

Goal state after:
case he
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k) * f (2 * k)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k + 1) * f (2 * k + 1)

Tactic:
·

Goal state after:
case ho
α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun k ↦ (-1) ^ (2 * k + 1) * f (2 * k + 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inl
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
hn : 0 ∈ mulSupport f
⊢ 0 ∈ Set.range PNat.val

pp: case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
h : n > 0
⊢ n ∈ Set.range PNat.val

Tactic:
·

Goal state after:
case inl
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
hn : 0 ∈ mulSupport f
⊢ 0 ∈ Set.range PNat.val
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
h : n > 0
⊢ n ∈ Set.range PNat.val

Tactic:
·

Goal state after:
case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
h : n > 0
⊢ n ∈ Set.range PNat.val
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
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
⊢ (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
⊢ (mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : β
h₀ : i ∉ ⋃ d, s d
⊢ (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : β
h₀ : i ∈ ⋃ d, s d
⊢ (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : IsEmpty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)

pp: case inr
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : Nonempty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : IsEmpty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : β
h₀ : i ∉ ⋃ d, s d
⊢ (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : β
h₀ : i ∉ ⋃ d, s d
⊢ (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h✝ : L.NeBot
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
hL : L.filter = ⊥
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

Tactic:
·

Goal state after:
case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h✝ : L.NeBot
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
hL : L.filter = ⊥
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

Tactic:
·

Goal state after:
case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
hL : L.filter = ⊥
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
·

Goal state after:
case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl.mp
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable (fun a ↦ ↑(f a)) L → Summable f L

pp: case inl.mpr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable f L → Summable (fun a ↦ ↑(f a)) L

Tactic:
·

Goal state after:
case inl.mp
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable (fun a ↦ ↑(f a)) L → Summable f L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
hβ : IsEmpty β
⊢ Multipliable (fun x ↦ 0) L

pp: case inr
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
hβ : Nonempty β
⊢ Multipliable (fun x ↦ 0) L

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
hβ : IsEmpty β
⊢ Multipliable (fun x ↦ 0) L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl.mpr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable f L → Summable (fun a ↦ ↑(f a)) L

Tactic:
·

Goal state after:
case inl.mpr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable f L → Summable (fun a ↦ ↑(f a)) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
hβ : Nonempty β
⊢ Multipliable (fun x ↦ 0) L

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
hβ : Nonempty β
⊢ Multipliable (fun x ↦ 0) L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
·

Goal state after:
case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
·

Goal state after:
case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
·

Goal state after:
case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case zero
ι : Sort u_1
n : ℕ
hn : 0 ≠ 0
⊢ (fun x ↦ x ^ 0) = ⇑(NNReal.powOrderIso 0 hn).withTopCongr

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

Tactic:
·

Goal state after:
case zero
ι : Sort u_1
n : ℕ
hn : 0 ≠ 0
⊢ (fun x ↦ x ^ 0) = ⇑(NNReal.powOrderIso 0 hn).withTopCongr
Module: Mathlib.Topology.Instances.NNReal.Lemmas

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

Tactic:
·

Goal state after:
case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
·

Goal state after:
case pos
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
·

Goal state after:
case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : IsEmpty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

pp: case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
·

Goal state after:
case inl
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : IsEmpty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
·

Goal state after:
case inr
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
h✝ : Nonempty ι
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n
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
⊢ ¬Bornology.IsBounded (image2 f s t)

Tactic:
obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2

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
⊢ ¬Bornology.IsBounded (image2 f s t)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: case inl
ι : 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
⊢ i ∈ Finset.univ → edist (Pi.single i x i) (Pi.single i y i) ≤ edist x y

pp: case inr
ι : 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
j : ι
h : i ≠ j
⊢ j ∈ Finset.univ → edist (Pi.single i x j) (Pi.single i y j) ≤ edist x y

Tactic:
·

Goal state after:
case inl
ι : 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
⊢ i ∈ Finset.univ → edist (Pi.single i x i) (Pi.single i y i) ≤ edist x y
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: case inr
ι : 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
j : ι
h : i ≠ j
⊢ j ∈ Finset.univ → edist (Pi.single i x j) (Pi.single i y j) ≤ edist x y

Tactic:
·

Goal state after:
case inr
ι : 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
j : ι
h : i ≠ j
⊢ j ∈ Finset.univ → edist (Pi.single i x j) (Pi.single i y j) ≤ edist x y
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:
rw [← h.isometry.preimage_closedEBall (h.symm x) r, h.apply_symm_apply]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2

Tactic:
by
    simp_rw [edist_pi_def, Finset.sup_univ_eq_iSup]
    exact (Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∈ s
⊢ x ∈ seqClosure s

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
⊢ x ∈ seqClosure s

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∈ s
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
⊢ x ∈ seqClosure s

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
⊢ x ∈ seqClosure s
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∃ m, ∃ᶠ (n : ℕ) in atTop, y n ∈ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
·

Goal state after:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∃ m, ∃ᶠ (n : ℕ) in atTop, y n ∈ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
·

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}