-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
    IsCycle g → IsCycle (g.extendDomain f)

Proof state:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb✝ : (g.extendDomain f) b ≠ b
hb : (g.extendDomain f) ↑(f (f.symm ⟨b, ⋯⟩)) ≠ ↑(f (f.symm ⟨b, ⋯⟩))
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
⊢ (g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))

Tactic:
simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb

Result:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb✝ : (g.extendDomain f) b ≠ b
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
hb : g (f.symm ⟨b, ⋯⟩) ≠ f.symm ⟨b, ⋯⟩
⊢ (g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))

Proof state:
case intro.intro.refine_1
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ ↑(f (g a)) ≠ ↑(f a)

Tactic:
exact Subtype.coe_injective.ne (f.injective.ne ha)

Result:
no goals

Proof state:
case intro.intro.refine_1
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ (g.extendDomain f) ↑(f a) ≠ ↑(f a)

Tactic:
rw [extendDomain_apply_image]

Result:
case intro.intro.refine_1
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ ↑(f (g a)) ≠ ↑(f a)

Proof state:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ g.IsCycle → (g.extendDomain f).IsCycle

Tactic:
rintro ⟨a, ha, ha'⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ (g.extendDomain f).IsCycle

Proof state:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
⊢ b = ↑(f (f.symm ⟨b, ⋯⟩))

Tactic:
rw [apply_symm_apply, Subtype.coe_mk]

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ (g.extendDomain f).IsCycle

Tactic:
refine ⟨f a, ?_, fun b hb => ?_⟩

Result:
case intro.intro.refine_1
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ (g.extendDomain f) ↑(f a) ≠ ↑(f a)

case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
⊢ (g.extendDomain f).SameCycle (↑(f a)) b

Proof state:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
⊢ (g.extendDomain f).SameCycle (↑(f a)) b

Tactic:
rw [h] at hb ⊢

Result:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb✝ : (g.extendDomain f) b ≠ b
hb : (g.extendDomain f) ↑(f (f.symm ⟨b, ⋯⟩)) ≠ ↑(f (f.symm ⟨b, ⋯⟩))
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
⊢ (g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))

Proof state:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
⊢ (g.extendDomain f).SameCycle (↑(f a)) b

Tactic:
have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
  rw [apply_symm_apply, Subtype.coe_mk]

Result:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
⊢ (g.extendDomain f).SameCycle (↑(f a)) b

Proof state:
case intro.intro.refine_2
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb✝ : (g.extendDomain f) b ≠ b
h : b = ↑(f (f.symm ⟨b, ⋯⟩))
hb : g (f.symm ⟨b, ⋯⟩) ≠ f.symm ⟨b, ⋯⟩
⊢ (g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))

Tactic:
exact (ha' hb).extendDomain

Result:
no goals