Theorem: IMOSL.Extra.CharTwo.forward_of_surj (IMOSLLean4/Extra/CharTwo/Hom.lean)

State before:
R : Type u_2
R' : Type u_1
inst✝² : AddMonoid R
inst✝¹ : CharTwo R
inst✝ : AddMonoid R'
φ : R →+ R'
h : Function.Surjective ⇑φ
x : R'
c : R
h0 : φ c = x
⊢ x + x = 0
Tactic:
rw [← h0, ← φ.map_add, add_self_eq_zero, φ.map_zero]
State after:
no goals