no goals
α : Type u_1
β : Type u_2
γ : Type ?u.143364
ι : Type ?u.143367
M : Type u_3
M' : Type ?u.143373
N : Type ?u.143376
P : Type ?u.143379
G : Type ?u.143382
H : Type ?u.143385
R : Type ?u.143388
S : Type ?u.143391
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (↑f a) b
classical
  ext x
  simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.143364
ι : Type ?u.143367
M : Type u_3
M' : Type ?u.143373
N : Type ?u.143376
P : Type ?u.143379
G : Type ?u.143382
H : Type ?u.143385
R : Type ?u.143388
S : Type ?u.143391
inst✝ : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ ↑(equivMapDomain f (single a b)) x = ↑(single (↑f a) b) x
α : Type u_1
β : Type u_2
γ : Type ?u.143364
ι : Type ?u.143367
M : Type u_3
M' : Type ?u.143373
N : Type ?u.143376
P : Type ?u.143379
G : Type ?u.143382
H : Type ?u.143385
R : Type ?u.143388
S : Type ?u.143391
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (↑f a) b
ext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.143364
ι : Type ?u.143367
M : Type u_3
M' : Type ?u.143373
N : Type ?u.143376
P : Type ?u.143379
G : Type ?u.143382
H : Type ?u.143385
R : Type ?u.143388
S : Type ?u.143391
inst✝ : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ ↑(equivMapDomain f (single a b)) x = ↑(single (↑f a) b) x
simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]