no goals
ι : Type u_3
σ : Type u_2
S : Type ?u.381766
R : Type u_1
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring R
inst✝⁶ : SetLike σ R
inst✝⁵ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁴ : CanonicallyOrderedAddMonoid ι
inst✝³ : SetLike.GradedMonoid A
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i
rw [eq_tsub_iff_add_eq_of_le h, add_comm]