Theorem: MetabelianGroup.Quotient.projection_surj (UnitConjecture/MetabelianGroup.lean)

State before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ Function.Surjective ↑(projection c)
Tactic:
intro q
State after:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ∃ a, ↑(projection c) a = q

State before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ∃ a, ↑(projection c) a = q
Tactic:
use ⟨(0 : K), q⟩
State after:
case h
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ↑(projection c) (0, q) = q

State before:
case h
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ↑(projection c) (0, q) = q
Tactic:
aesop
State after:
no goals