α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2✝ : ↑(single x y) ht1 = r
ht2 : (if x = ht1 then y else 0) = r
⊢ (if x = ht1 then y else 0) ∈ {y}
α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2 : ↑(single x y) ht1 = r
⊢ ↑(single x y) ht1 ∈ {y}
rw [single_apply] at ht2⊢
case inl
α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2✝ : ↑(single x y) ht1 = r
h✝ : x = ht1
ht2 : y = r
⊢ y ∈ {y}

case inr
α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2✝ : ↑(single x y) ht1 = r
h✝ : ¬x = ht1
ht2 : 0 = r
⊢ 0 ∈ {y}
α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2✝ : ↑(single x y) ht1 = r
ht2 : (if x = ht1 then y else 0) = r
⊢ (if x = ht1 then y else 0) ∈ {y}
split_ifs  at ht2⊢
no goals
case inl
α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2✝ : ↑(single x y) ht1 = r
h✝ : x = ht1
ht2 : y = r
⊢ y ∈ {y}
exact Finset.mem_singleton_self _
no goals
case inr
α : Type u_2
β : Type ?u.482925
γ : Type ?u.482928
ι : Type ?u.482931
M : Type u_1
M' : Type ?u.482937
N : Type ?u.482940
P : Type ?u.482943
G : Type ?u.482946
H : Type ?u.482949
R : Type ?u.482952
S : Type ?u.482955
inst✝ : Zero M
x : α
y r : M
hr : r ∈ frange (single x y)
t : r ≠ 0
ht1 : α
ht2✝ : ↑(single x y) ht1 = r
h✝ : ¬x = ht1
ht2 : 0 = r
⊢ 0 ∈ {y}
exact (t ht2.symm).elim