case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
y : OreLocalization R S
r✝ : R
s✝ : { x // x ∈ S }
⊢ r✝ /ₒ s✝ + y = y + r✝ /ₒ s✝
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
x y : OreLocalization R S
⊢ x + y = y + x
induction x using OreLocalization.ind
case c.c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝¹ : R
s✝¹ : { x // x ∈ S }
r✝ : R
s✝ : { x // x ∈ S }
⊢ r✝¹ /ₒ s✝¹ + r✝ /ₒ s✝ = r✝ /ₒ s✝ + r✝¹ /ₒ s✝¹
case c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
y : OreLocalization R S
r✝ : R
s✝ : { x // x ∈ S }
⊢ r✝ /ₒ s✝ + y = y + r✝ /ₒ s✝
induction y using OreLocalization.ind
case c.c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝¹ : R
s✝¹ : { x // x ∈ S }
r✝ : R
s✝ : { x // x ∈ S }
⊢ OreLocalization.add' (r✝, s✝).fst (r✝, s✝).snd (r✝¹ /ₒ s✝¹) = r✝ /ₒ s✝ + r✝¹ /ₒ s✝¹
case c.c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝¹ : R
s✝¹ : { x // x ∈ S }
r✝ : R
s✝ : { x // x ∈ S }
⊢ r✝¹ /ₒ s✝¹ + r✝ /ₒ s✝ = r✝ /ₒ s✝ + r✝¹ /ₒ s✝¹
change add' _ _ (_ /ₒ _) = _
no goals
case c.c
R : Type u_1
inst✝¹ : Semiring R
S : Submonoid R
inst✝ : OreSet S
r✝¹ : R
s✝¹ : { x // x ∈ S }
r✝ : R
s✝ : { x // x ∈ S }
⊢ OreLocalization.add' (r✝, s✝).fst (r✝, s✝).snd (r✝¹ /ₒ s✝¹) = r✝ /ₒ s✝ + r✝¹ /ₒ s✝¹
apply add'_comm