α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
⊢ HasSum (Int.rec f g) (a + b)
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (Int.rec f g) (a + b)
have h₁ : Injective ((↑) : ℕ → ℤ) := @Int.ofNat.inj
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ HasSum (Int.rec f g) (a + b)
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
⊢ HasSum (Int.rec f g) (a + b)
have h₂ : Injective Int.negSucc := @Int.negSucc.inj
no goals
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ HasSum (Int.rec f g) (a + b)
exact HasSum.add_isCompl this (h₁.hasSum_range_iff.mpr hf) (h₂.hasSum_range_iff.mpr hg)
case disjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

case codisjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
constructor
case disjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥
case disjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)
rw [disjoint_iff_inf_le]
no goals
case disjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥
rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩
case codisjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc
case codisjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
rw [codisjoint_iff_le_sup]
case codisjoint.ofNat
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
i : ℕ
a✝ : Int.ofNat i ∈ ⊤
⊢ Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

case codisjoint.negSucc
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
j : ℕ
a✝ : Int.negSucc j ∈ ⊤
⊢ Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc
case codisjoint
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
⊢ ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc
rintro (i | j) _
no goals
case codisjoint.ofNat
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
i : ℕ
a✝ : Int.ofNat i ∈ ⊤
⊢ Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

case codisjoint.negSucc
α : Type u_1
β : Type ?u.474506
γ : Type ?u.474509
δ : Type ?u.474512
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f g : ℕ → α
hf : HasSum f a
hg : HasSum g b
h₁ : Injective Nat.cast
h₂ : Injective Int.negSucc
j : ℕ
a✝ : Int.negSucc j ∈ ⊤
⊢ Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc
exacts [Or.inl ⟨_, rfl⟩, Or.inr ⟨_, rfl⟩]