case intro.intro.intro.intro
ι : Type ?u.2071598
α : Type u_2
β : Type u_1
f✝ g : Perm α
s t : Set α
a✝ b✝ x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : IsCycleOn g s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ SameCycle (Perm.extendDomain g f) ((Subtype.val ∘ ↑f) a) ((Subtype.val ∘ ↑f) b)
ι : Type ?u.2071598
α : Type u_2
β : Type u_1
f✝ g : Perm α
s t : Set α
a b x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : IsCycleOn g s
⊢ ∀ ⦃x : β⦄, x ∈ Subtype.val ∘ ↑f '' s → ∀ ⦃y : β⦄, y ∈ Subtype.val ∘ ↑f '' s → SameCycle (Perm.extendDomain g f) x y
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
no goals
case intro.intro.intro.intro
ι : Type ?u.2071598
α : Type u_2
β : Type u_1
f✝ g : Perm α
s t : Set α
a✝ b✝ x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : IsCycleOn g s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ SameCycle (Perm.extendDomain g f) ((Subtype.val ∘ ↑f) a) ((Subtype.val ∘ ↑f) b)
exact (h.2 ha hb).extendDomain