case a
α : Type ?u.10924
M₀ : Type ?u.10927
G₀ : Type u_1
M₀' : Type ?u.10933
G₀' : Type ?u.10936
F : Type ?u.10939
F' : Type ?u.10942
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b : G₀
h : optParam (1 ≠ 0) (_ : 1 ≠ 0)
⊢ ↑(mk0 1 h) = ↑1
α : Type ?u.10924
M₀ : Type ?u.10927
G₀ : Type u_1
M₀' : Type ?u.10933
G₀' : Type ?u.10936
F : Type ?u.10939
F' : Type ?u.10942
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b : G₀
h : optParam (1 ≠ 0) (_ : 1 ≠ 0)
⊢ mk0 1 h = 1
ext
no goals
case a
α : Type ?u.10924
M₀ : Type ?u.10927
G₀ : Type u_1
M₀' : Type ?u.10933
G₀' : Type ?u.10936
F : Type ?u.10939
F' : Type ?u.10942
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b : G₀
h : optParam (1 ≠ 0) (_ : 1 ≠ 0)
⊢ ↑(mk0 1 h) = ↑1
rfl