Theorem: Cocycle.left_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 0 q = 0
Tactic:
have := ccl.cocycle_condition 0 0 q
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 0 0 + c (0 + 0) q = 0 +ᵥ c 0 q + c 0 (0 + q)
⊢ c 0 q = 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 0 0 + c (0 + 0) q = 0 +ᵥ c 0 q + c 0 (0 + q)
⊢ c 0 q = 0
Tactic:
rw [add_zero, zero_add, ccl.cocycle_zero, zero_add, zero_vadd] 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 0 q = c 0 q + c 0 q
⊢ c 0 q = 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 0 q = c 0 q + c 0 q
⊢ c 0 q = 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 0 q = 0
⊢ c 0 q = 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 0 q = 0
⊢ c 0 q = 0
Tactic:
assumption
State after:
no goals