internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.comp_assoc
Proof state before:
R✝ : Type u
inst✝¹³ : CommRing R✝
M✝ : Type u_1
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R✝ M✝
N✝ : Type u_2
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommGroup P
inst✝² : Module R P
Q : Type u_6
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
⊢ h.comp (g.comp f) = (h.comp g).comp f
Tactic:
ext
Proof state after:
case toFun'.h.h.h.h
R✝ : Type u
inst✝¹³ : CommRing R✝
M✝ : Type u_1
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R✝ M✝
N✝ : Type u_2
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommGroup P
inst✝² : Module R P
Q : Type u_6
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.comp (g.comp f)).toFun' x✝³ x✝ = ((h.comp g).comp f).toFun' x✝³ x✝
Theorem: PolynomialMap.comp_assoc
Proof state before:
case toFun'.h.h.h.h
R✝ : Type u
inst✝¹³ : CommRing R✝
M✝ : Type u_1
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R✝ M✝
N✝ : Type u_2
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommGroup P
inst✝² : Module R P
Q : Type u_6
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.comp (g.comp f)).toFun' x✝³ x✝ = ((h.comp g).comp f).toFun' x✝³ x✝
Tactic:
simp only [comp_toFun']
Proof state after:
case toFun'.h.h.h.h
R✝ : Type u
inst✝¹³ : CommRing R✝
M✝ : Type u_1
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R✝ M✝
N✝ : Type u_2
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommGroup P
inst✝² : Module R P
Q : Type u_6
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.toFun' x✝³ ∘ g.toFun' x✝³ ∘ f.toFun' x✝³) x✝ = ((h.toFun' x✝³ ∘ g.toFun' x✝³) ∘ f.toFun' x✝³) x✝
Theorem: PolynomialMap.comp_assoc
Proof state before:
case toFun'.h.h.h.h
R✝ : Type u
inst✝¹³ : CommRing R✝
M✝ : Type u_1
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R✝ M✝
N✝ : Type u_2
inst✝¹⁰ : AddCommGroup N✝
inst✝⁹ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommGroup P
inst✝² : Module R P
Q : Type u_6
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
f : M →ₚ[R] N
g : N →ₚ[R] P
h : P →ₚ[R] Q
x✝³ : Type u
x✝² : CommRing x✝³
x✝¹ : Algebra R x✝³
x✝ : x✝³ ⊗[R] M
⊢ (h.toFun' x✝³ ∘ g.toFun' x✝³ ∘ f.toFun' x✝³) x✝ = ((h.toFun' x✝³ ∘ g.toFun' x✝³) ∘ f.toFun' x✝³) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: tprod_one_le
Proof state before:
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
⊢ 1 ≤ ∏' (i : ι), g i
Tactic:
by_cases hg : Multipliable g
Proof state after:
case pos
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

case neg
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i
Theorem: tprod_one_le
Proof state before:
case pos
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i
Tactic:
exact hg.hasProd.one_le h
Proof state after:
no goals
Theorem: tprod_one_le
Proof state before:
case neg
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i
Tactic:
simp [tprod_eq_one_of_not_multipliable hg]
Proof state after:
no goals
Theorem: tprod_pos
Proof state before:
ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ 1 < ∏' (i : ι), g i
Tactic:
rw [← tprod_one]
Proof state after:
ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏' (x : ?m.11469), 1 < ∏' (i : ι), g i

ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ Type ?u.11467
Theorem: tprod_pos
Proof state before:
ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏' (x : ?m.11469), 1 < ∏' (i : ι), g i

ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ Type ?u.11467
Tactic:
exact tprod_lt_tprod hg hi multipliable_one hprod
Proof state after:
no goals
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : Tendsto f cofinite (nhds 0)
⊢ (support f).Finite
Tactic:
rw [nhds_discrete, tendsto_pure] at hf
Proof state after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
⊢ (support f).Finite
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
⊢ (support f).Finite
Tactic:
obtain ⟨s, H, p⟩ := Eventually.exists_mem hf
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ (support f).Finite
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ (support f).Finite
Tactic:
apply Finite.subset H
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ support f ⊆ sᶜ
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ support f ⊆ sᶜ
Tactic:
intro x hx
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∈ sᶜ
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∈ sᶜ
Tactic:
rw [mem_compl_iff]
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∉ s
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∉ s
Tactic:
by_contra hxs
Proof state after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
hxs : x ∈ s
⊢ False
Theorem: Function.finite_support_of_tendsto_zero
Proof state before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
hxs : x ∈ s
⊢ False
Tactic:
exact hx (p x hxs)
Proof state after:
no goals
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
hf : Summable f
⊢ Tendsto f cofinite (nhds 0)
Tactic:
obtain ⟨a, ha⟩ := hf
Proof state after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : HasSum f a
⊢ Tendsto f cofinite (nhds 0)
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : HasSum f a
⊢ Tendsto f cofinite (nhds 0)
Tactic:
rw [HasSum, tendsto_atTop_nhds] at ha
Proof state after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ Tendsto f cofinite (nhds 0)
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ Tendsto f cofinite (nhds 0)
Tactic:
rw [tendsto_nhds]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ ∀ (s : Set α), IsOpen s → 0 ∈ s → f ⁻¹' s ∈ cofinite
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ ∀ (s : Set α), IsOpen s → 0 ∈ s → f ⁻¹' s ∈ cofinite
Tactic:
intro U₀ hU₀ memU₀
Proof state after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
suffices hU₁ : ∃ U₁ : Set α, IsOpen U₁ ∧ (0 : α) ∈ U₁ ∧ U₁ - U₁ ≤ U₀ by
  obtain ⟨U₁, hU₁, memU₁, addU₁_subset⟩ := hU₁
  obtain ⟨S, hS⟩ :=
    ha ((fun x => x - a) ⁻¹' U₁) (by simp only [memU₁, Set.mem_preimage, sub_self])
      (IsOpen.preimage (continuous_sub_right a) hU₁)
  apply S.finite_toSet.subset
  intro i hi
  by_contra his
  apply hi
  apply addU₁_subset
  use (insert i S).sum f - a,
    hS (insert i S) (subset_insert i S),
    S.sum f - a,
    hS S le_rfl
  simp only [sum_insert his, sub_sub_sub_cancel_right, add_sub_cancel_right]
Proof state after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
hU₁ : ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
obtain ⟨U₁, hU₁, memU₁, addU₁_subset⟩ := hU₁
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
obtain ⟨S, hS⟩ :=
  ha ((fun x => x - a) ⁻¹' U₁) (by simp only [memU₁, Set.mem_preimage, sub_self])
    (IsOpen.preimage (continuous_sub_right a) hU₁)
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ f ⁻¹' U₀ ∈ cofinite
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ f ⁻¹' U₀ ∈ cofinite
Tactic:
apply S.finite_toSet.subset
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ (f ⁻¹' U₀)ᶜ ⊆ ↑S
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
⊢ (f ⁻¹' U₀)ᶜ ⊆ ↑S
Tactic:
intro i hi
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
⊢ i ∈ ↑S
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
⊢ i ∈ ↑S
Tactic:
by_contra his
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ False
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ False
Tactic:
apply hi
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ i ∈ f ⁻¹' U₀
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ i ∈ f ⁻¹' U₀
Tactic:
apply addU₁_subset
Proof state after:
case intro.intro.intro.intro.a
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ f i ∈ U₁ - U₁
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro.a
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ f i ∈ U₁ - U₁
Tactic:
use (insert i S).sum f - a,
  hS (insert i S) (subset_insert i S),
  S.sum f - a,
  hS S le_rfl
Proof state after:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ (fun x x_1 => x - x_1) ((insert i S).sum f - a) (S.sum f - a) = f i
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
S : Finset ι
hS : ∀ (n : Finset ι), S ≤ n → ∑ b ∈ n, f b ∈ (fun x => x - a) ⁻¹' U₁
i : ι
hi : i ∈ (f ⁻¹' U₀)ᶜ
his : i ∉ ↑S
⊢ (fun x x_1 => x - x_1) ((insert i S).sum f - a) (S.sum f - a) = f i
Tactic:
simp only [sum_insert his, sub_sub_sub_cancel_right, add_sub_cancel_right]
Proof state after:
no goals
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
U₁ : Set α
hU₁ : IsOpen U₁
memU₁ : 0 ∈ U₁
addU₁_subset : U₁ - U₁ ≤ U₀
⊢ a ∈ (fun x => x - a) ⁻¹' U₁
Tactic:
simp only [memU₁, Set.mem_preimage, sub_self]
Proof state after:
no goals