case intro.intro
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
⊢ ∃ F, Semiconj ↑F ↑↑f₁ ↑↑f₂
f g f₁ f₂ : CircleDeg1Lift
h₁ : IsUnit f₁
h₂ : IsUnit f₂
h : τ f₁ = τ f₂
⊢ ∃ F, Semiconj ↑F ↑f₁ ↑f₂
rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩
no goals
case intro.intro
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
⊢ ∃ F, Semiconj ↑F ↑↑f₁ ↑↑f₂
exact units_semiconj_of_translationNumber_eq h