Theorem: Cocycle.right_id (UnitConjecture/Cocycle.lean)

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
⊢ c q 0 = 0
Tactic:
have := ccl.cocycle_condition q 0 0
State after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c (q + 0) 0 = q +ᵥ c 0 0 + c q (0 + 0)
⊢ c q 0 = 0

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c (q + 0) 0 = q +ᵥ c 0 0 + c q (0 + 0)
⊢ c q 0 = 0
Tactic:
rw [add_zero, zero_add, ccl.cocycle_zero] at this
State after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c q 0 = q +ᵥ 0 + c q 0
⊢ c q 0 = 0

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 + c q 0 = q +ᵥ 0 + c q 0
⊢ c q 0 = 0
Tactic:
simp at this
State after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 = q +ᵥ 0
⊢ c q 0 = 0

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddGroup K
c : Q → Q → K
ccl : Cocycle c
q : Q
this : c q 0 = q +ᵥ 0
⊢ c q 0 = 0
Tactic:
rw [this, AutAction.vadd_zero]
State after:
no goals