internlm/Lean-Github huggingface dataset:
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
⊢ rTensorAlgHom (x ⊗ₜ[R] n) = ↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)
Tactic:
apply Finsupp.ext
Proof state after:
case a.h.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
⊢ ∀ (a : α), (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
⊢ ∀ (a : α), (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Tactic:
intro a
Proof state after:
case a.h.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Tactic:
rw [rTensorAlgHom_apply_tmul_apply, ← finsuppLeft_apply_tmul_apply]
Proof state after:
case a.h.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((finsuppLeft R M N α) (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap
Proof state before:
case a.h.h.h
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α
n : N
a : α
⊢ ((finsuppLeft R M N α) (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Tactic:
rfl
Proof state after:
no goals
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap'
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ rTensorAlgHom.toLinearMap = ↑(finsuppLeft R M N α)
Tactic:
rw [rTensorAlgHom_toLinearMap]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ ↑(finsuppLeft' R M N α R) = ↑(finsuppLeft R M N α)
Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap'
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ ↑(finsuppLeft' R M N α R) = ↑(finsuppLeft R M N α)
Tactic:
rfl
Proof state after:
no goals
Theorem: MonoidAlgebra.rTensorAlgHom_apply_eq
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α ⊗[R] N
⊢ rTensorAlgHom x = (finsuppLeft' R M N α S) x
Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
Proof state after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α ⊗[R] N
⊢ ↑(finsuppLeft' R M N α S) x = (finsuppLeft' R M N α S) x
Theorem: MonoidAlgebra.rTensorAlgHom_apply_eq
Proof state before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α ⊗[R] N
⊢ ↑(finsuppLeft' R M N α S) x = (finsuppLeft' R M N α S) x
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.Finite.support_of_summable
Proof state before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
h : Summable f
⊢ (Function.support f).Finite
Tactic:
obtain ⟨a, ha⟩ := h
Proof state after:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : HasSum f a
⊢ (Function.support f).Finite
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : HasSum f a
⊢ (Function.support f).Finite
Tactic:
simp only [HasSum] at ha
Proof state after:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : Filter.Tendsto (fun s => ∑ b ∈ s, f b) Filter.atTop (nhds a)
⊢ (Function.support f).Finite
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : Filter.Tendsto (fun s => ∑ b ∈ s, f b) Filter.atTop (nhds a)
⊢ (Function.support f).Finite
Tactic:
classical
simp_rw [tendsto_atTop_nhds] at ha
obtain ⟨s, hs⟩ := ha {a} rfl (isOpen_discrete _)
apply Set.Finite.subset s.finite_toSet
intro b
rw [Function.mem_support, not_imp_comm]
intro hb
let hs' := hs (insert b s) (s.subset_insert b)
specialize hs s (subset_of_eq rfl)
simp only [Set.mem_singleton_iff] at hs hs'
simpa [Finset.sum_insert hb, hs, add_left_eq_self] using hs'
Proof state after:
no goals
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : Filter.Tendsto (fun s => ∑ b ∈ s, f b) Filter.atTop (nhds a)
⊢ (Function.support f).Finite
Tactic:
simp_rw [tendsto_atTop_nhds] at ha
Proof state after:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ (Function.support f).Finite
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ (Function.support f).Finite
Tactic:
obtain ⟨s, hs⟩ := ha {a} rfl (isOpen_discrete _)
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ (Function.support f).Finite
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ (Function.support f).Finite
Tactic:
apply Set.Finite.subset s.finite_toSet
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ Function.support f ⊆ ↑s
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ Function.support f ⊆ ↑s
Tactic:
intro b
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∈ Function.support f → b ∈ ↑s
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∈ Function.support f → b ∈ ↑s
Tactic:
rw [Function.mem_support, not_imp_comm]
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∉ ↑s → f b = 0
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∉ ↑s → f b = 0
Tactic:
intro hb
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
⊢ f b = 0
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
⊢ f b = 0
Tactic:
let hs' := hs (insert b s) (s.subset_insert b)
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs (insert b s) (Finset.subset_insert b s)
⊢ f b = 0
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs (insert b s) (Finset.subset_insert b s)
⊢ f b = 0
Tactic:
specialize hs s (subset_of_eq rfl)
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs✝ (insert b s) (Finset.subset_insert b s)
hs : ∑ b ∈ s, f b ∈ {a}
⊢ f b = 0
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs✝ (insert b s) (Finset.subset_insert b s)
hs : ∑ b ∈ s, f b ∈ {a}
⊢ f b = 0
Tactic:
simp only [Set.mem_singleton_iff] at hs hs'
Proof state after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs : ∑ b ∈ s, f b = a
hs' : ∑ b ∈ insert b s, f b = a
⊢ f b = 0
Theorem: Set.Finite.support_of_summable
Proof state before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs : ∑ b ∈ s, f b = a
hs' : ∑ b ∈ insert b s, f b = a
⊢ f b = 0
Tactic:
simpa [Finset.sum_insert hb, hs, add_left_eq_self] using hs'
Proof state after:
no goals
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ (a + b) ^ (m + n).pred = 0
Tactic:
rw [add_pow]
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∑ m_1 ∈ Finset.range ((m + n).pred + 1), a ^ m_1 * b ^ ((m + n).pred - m_1) * ↑((m + n).pred.choose m_1) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∑ m_1 ∈ Finset.range ((m + n).pred + 1), a ^ m_1 * b ^ ((m + n).pred - m_1) * ↑((m + n).pred.choose m_1) = 0
Tactic:
apply Finset.sum_eq_zero
Proof state after:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∀ x ∈ Finset.range ((m + n).pred + 1), a ^ x * b ^ ((m + n).pred - x) * ↑((m + n).pred.choose x) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
⊢ ∀ x ∈ Finset.range ((m + n).pred + 1), a ^ x * b ^ ((m + n).pred - x) * ↑((m + n).pred.choose x) = 0
Tactic:
intro k hk
Proof state after:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k ∈ Finset.range ((m + n).pred + 1)
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k ∈ Finset.range ((m + n).pred + 1)
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
simp only [Finset.mem_range] at hk
Proof state after:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case h
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
by_cases h : k < m
Proof state after:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0

case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : ¬k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
have : n ≤ (m + n).pred - k  := by
  rw [Nat.le_sub_iff_add_le (Nat.le_of_lt_succ hk), add_comm]
  rw [Nat.le_pred_iff_lt (lt_of_le_of_lt (zero_le k) (Nat.lt_add_right n h))]
  exact Nat.add_lt_add_right h n
Proof state after:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
rw [← Nat.add_sub_of_le this, pow_add, hb]
Proof state after:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * (0 * b ^ ((m + n).pred - k - n)) * ↑((m + n).pred.choose k) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case pos
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
this : n ≤ (m + n).pred - k
⊢ a ^ k * (0 * b ^ ((m + n).pred - k - n)) * ↑((m + n).pred.choose k) = 0
Tactic:
simp only [zero_mul, mul_zero]
Proof state after:
no goals
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ n ≤ (m + n).pred - k
Tactic:
rw [Nat.le_sub_iff_add_le (Nat.le_of_lt_succ hk), add_comm]
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n ≤ (m + n).pred
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n ≤ (m + n).pred
Tactic:
rw [Nat.le_pred_iff_lt (lt_of_le_of_lt (zero_le k) (Nat.lt_add_right n h))]
Proof state after:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n < m + n
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : k < m
⊢ k + n < m + n
Tactic:
exact Nat.add_lt_add_right h n
Proof state after:
no goals
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : ¬k < m
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
simp only [not_lt] at h
Proof state after:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ a ^ k * b ^ ((m + n).pred - k) * ↑((m + n).pred.choose k) = 0
Tactic:
rw [← Nat.add_sub_of_le h, pow_add, ha]
Proof state after:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ 0 * a ^ (k - m) * b ^ ((m + n).pred - (m + (k - m))) * ↑((m + n).pred.choose (m + (k - m))) = 0
Theorem: add_pow_add_pred_eq_zero_of_pow_eq_zero
Proof state before:
case neg
α : Type u_1
inst✝ : CommSemiring α
a b : α
m n : ℕ
ha : a ^ m = 0
hb : b ^ n = 0
k : ℕ
hk : k < (m + n).pred + 1
h : m ≤ k
⊢ 0 * a ^ (k - m) * b ^ ((m + n).pred - (m + (k - m))) * ↑((m + n).pred.choose (m + (k - m))) = 0
Tactic:
simp only [zero_mul]
Proof state after:
no goals
Theorem: IsNilpotent.add
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
a b : α
ha : IsNilpotent a
hb : IsNilpotent b
⊢ IsNilpotent (a + b)
Tactic:
obtain ⟨m, ha⟩ := ha
Proof state after:
case intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
hb : IsNilpotent b
m : ℕ
ha : a ^ m = 0
⊢ IsNilpotent (a + b)
Theorem: IsNilpotent.add
Proof state before:
case intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
hb : IsNilpotent b
m : ℕ
ha : a ^ m = 0
⊢ IsNilpotent (a + b)
Tactic:
obtain ⟨n, hb⟩ := hb
Proof state after:
case intro.intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
m : ℕ
ha : a ^ m = 0
n : ℕ
hb : b ^ n = 0
⊢ IsNilpotent (a + b)
Theorem: IsNilpotent.add
Proof state before:
case intro.intro
α : Type u_1
inst✝ : CommSemiring α
a b : α
m : ℕ
ha : a ^ m = 0
n : ℕ
hb : b ^ n = 0
⊢ IsNilpotent (a + b)
Tactic:
exact ⟨_, add_pow_add_pred_eq_zero_of_pow_eq_zero ha hb⟩
Proof state after:
no goals
Theorem: IsNilpotent.finset_sum
Proof state before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
s : Finset β
hf : ∀ b ∈ s, IsNilpotent (f b)
⊢ IsNilpotent (s.sum f)
Tactic:
classical
induction s using Finset.induction_on with
  | empty => simp only [Finset.sum_empty, IsNilpotent.zero]
  | @insert b s hb hs =>
    rw [Finset.sum_insert hb]
    apply IsNilpotent.add
    exact hf b (s.mem_insert_self b)
    exact hs (fun b hb ↦ hf b (by exact Finset.mem_insert_of_mem hb))
Proof state after:
no goals