-- Mathlib/GroupTheory/Perm/Support.lean
theorem ofSubtype_swap_eq {p : α → Prop} [DecidablePred p] (x y : Subtype p) :
    ofSubtype (Equiv.swap x y) = Equiv.swap ↑x ↑y :=
  Equiv.ext fun z => by
    by_cases hz : p z
    · rw [swap_apply_def, ofSubtype_apply_of_mem _ hz]
      split_ifs with hzx hzy
      · simp_rw [hzx, Subtype.coe_eta, swap_apply_left]
      · simp_rw [hzy, Subtype.coe_eta, swap_apply_right]
      · rw [swap_apply_of_ne_of_ne] <;>
        simp [Subtype.ext_iff, *]
    · rw [ofSubtype_apply_of_not_mem _ hz, swap_apply_of_ne_of_ne]
      · intro h
        apply hz
        rw [h]
        exact Subtype.prop x
      intro h
      apply hz
      rw [h]
      exact Subtype.prop y

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑x

Tactic:
intro h

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ False

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p ↑x

Tactic:
exact Subtype.prop x

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : z = ↑y
⊢ ↑((swap x y) ⟨z, hz⟩) = ↑x

Tactic:
simp_rw [hzy, Subtype.coe_eta, swap_apply_right]

Result:
no goals

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p ↑y

Tactic:
exact Subtype.prop y

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ (ofSubtype (swap x y)) z = (swap ↑x ↑y) z

Tactic:
rw [swap_apply_def, ofSubtype_apply_of_mem _ hz]

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ ↑((swap x y) ⟨z, hz⟩) = if z = ↑x then ↑y else if z = ↑y then ↑x else z

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ False

Tactic:
apply hz

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p z

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p z

Tactic:
rw [h]

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p ↑y

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ (ofSubtype (swap x y)) z = (swap ↑x ↑y) z

Tactic:
rw [ofSubtype_apply_of_not_mem _ hz, swap_apply_of_ne_of_ne]

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑x

case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p z

Tactic:
rw [h]

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p ↑x

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ ↑((swap x y) ⟨z, hz⟩) = if z = ↑x then ↑y else if z = ↑y then ↑x else z

Tactic:
split_ifs with hzx hzy

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : z = ↑x
⊢ ↑((swap x y) ⟨z, hz⟩) = ↑y

case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : z = ↑y
⊢ ↑((swap x y) ⟨z, hz⟩) = ↑x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ ↑((swap x y) ⟨z, hz⟩) = z

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
⊢ (ofSubtype (swap x y)) z = (swap ↑x ↑y) z

Tactic:
by_cases hz : p z

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ (ofSubtype (swap x y)) z = (swap ↑x ↑y) z

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ (ofSubtype (swap x y)) z = (swap ↑x ↑y) z

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ ↑((swap x y) ⟨z, hz⟩) = z

Tactic:
rw [swap_apply_of_ne_of_ne] <;>
simp [Subtype.ext_iff, *]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : z = ↑x
⊢ ↑((swap x y) ⟨z, hz⟩) = ↑y

Tactic:
simp_rw [hzx, Subtype.coe_eta, swap_apply_left]

Result:
no goals

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y

Tactic:
intro h

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ False

Proof state:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ False

Tactic:
apply hz

Result:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p z