case intro.intro
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
⊢ IsCycle (extendDomain g f)
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ IsCycle g → IsCycle (extendDomain g f)
rintro ⟨a, ha, ha'⟩
case intro.intro.refine'_1
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
⊢ ↑(extendDomain g f) ↑(↑f a) ≠ ↑(↑f a)

case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb : ↑(extendDomain g f) b ≠ b
⊢ SameCycle (extendDomain g f) (↑(↑f a)) b
case intro.intro
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
⊢ IsCycle (extendDomain g f)
refine' ⟨f a, _, fun b hb => _⟩
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb : ↑(extendDomain g f) b ≠ b
h : b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
⊢ SameCycle (extendDomain g f) (↑(↑f a)) b
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb : ↑(extendDomain g f) b ≠ b
⊢ SameCycle (extendDomain g f) (↑(↑f a)) b
have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
  rw [apply_symm_apply, Subtype.coe_mk]
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb✝ : ↑(extendDomain g f) b ≠ b
hb :
  ↑(extendDomain g f) ↑(↑f (↑f.symm { val := b, property := (_ : p b) })) ≠
    ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
h : b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
⊢ SameCycle (extendDomain g f) ↑(↑f a) ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb : ↑(extendDomain g f) b ≠ b
h : b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
⊢ SameCycle (extendDomain g f) (↑(↑f a)) b
rw [h] at hb⊢
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb✝ : ↑(extendDomain g f) b ≠ b
h : b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
hb : ↑g (↑f.symm { val := b, property := (_ : p b) }) ≠ ↑f.symm { val := b, property := (_ : p b) }
⊢ SameCycle (extendDomain g f) ↑(↑f a) ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb✝ : ↑(extendDomain g f) b ≠ b
hb :
  ↑(extendDomain g f) ↑(↑f (↑f.symm { val := b, property := (_ : p b) })) ≠
    ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
h : b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
⊢ SameCycle (extendDomain g f) ↑(↑f a) ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb
no goals
case intro.intro.refine'_2
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb✝ : ↑(extendDomain g f) b ≠ b
h : b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
hb : ↑g (↑f.symm { val := b, property := (_ : p b) }) ≠ ↑f.symm { val := b, property := (_ : p b) }
⊢ SameCycle (extendDomain g f) ↑(↑f a) ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
exact (ha' hb).extendDomain
case intro.intro.refine'_1
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
⊢ ↑(↑f (↑g a)) ≠ ↑(↑f a)
case intro.intro.refine'_1
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
⊢ ↑(extendDomain g f) ↑(↑f a) ≠ ↑(↑f a)
rw [extendDomain_apply_image]
no goals
case intro.intro.refine'_1
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
⊢ ↑(↑f (↑g a)) ≠ ↑(↑f a)
exact Subtype.coe_injective.ne (f.injective.ne ha)
no goals
ι : Type ?u.344602
α : Type u_2
β : Type u_1
f✝ g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : ↑g a ≠ a
ha' : ∀ ⦃y : α⦄, ↑g y ≠ y → SameCycle g a y
b : β
hb : ↑(extendDomain g f) b ≠ b
⊢ b = ↑(↑f (↑f.symm { val := b, property := (_ : p b) }))
rw [apply_symm_apply, Subtype.coe_mk]