no goals
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
n : Multiplicative ℤ
⊢ τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) n) =
    τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) n)
simp [h]
no goals
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ↑F ↑(↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ↑(↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ↑F ↑↑f₁ ↑↑f₂
simpa using hF (Multiplicative.ofAdd 1)