α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
⊢ Disjoint (Perm.extendDomain σ f) (Perm.extendDomain τ f)
intro b
case pos
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : p b
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b

case neg
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : ¬p b
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
by_cases pb : p b
case pos.refine'_2
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : Disjoint σ τ
b : β
pb : p b
h : ↑τ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
⊢ ↑(Perm.extendDomain τ f) b = b
case pos.refine'_2
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : p b
⊢ ↑τ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb } → ↑(Perm.extendDomain τ f) b = b
intro h
no goals
case pos.refine'_2
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : Disjoint σ τ
b : β
pb : p b
h : ↑τ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
⊢ ↑(Perm.extendDomain τ f) b = b
rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
case neg.h
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : ¬p b
⊢ ↑(Perm.extendDomain σ f) b = b
case neg
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : ¬p b
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
left
no goals
case neg.h
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : ¬p b
⊢ ↑(Perm.extendDomain σ f) b = b
rw [extendDomain_apply_not_subtype _ _ pb]