case ofNat
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0

case negSucc
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
z : ℤ
⊢ ↑z ∈ A 0
induction z
case ofNat
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑a✝ ∈ A 0
case ofNat
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0
rw [Int.ofNat_eq_coe, Int.cast_ofNat]
no goals
case ofNat
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑a✝ ∈ A 0
exact SetLike.nat_cast_mem_graded _ _
case negSucc
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0
case negSucc
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0
rw [Int.cast_negSucc]
no goals
case negSucc
ι : Type u_1
σ : Type u_3
S : Type ?u.28560
R : Type u_2
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0
exact neg_mem (SetLike.nat_cast_mem_graded _ _)