Theorem: MetabelianGroup.Kernel.inclusion_inj (UnitConjecture/MetabelianGroup.lean)

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ Function.Injective ↑(inclusion c)
Tactic:
intros _ _
State after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
a₁✝ a₂✝ : Multiplicative K
⊢ ↑(inclusion c) a₁✝ = ↑(inclusion c) a₂✝ → a₁✝ = a₂✝

State before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
a₁✝ a₂✝ : Multiplicative K
⊢ ↑(inclusion c) a₁✝ = ↑(inclusion c) a₂✝ → a₁✝ = a₂✝
Tactic:
simp [Kernel.inclusion]
State after:
no goals