-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_extend_domain (f : α ≃ Subtype p) {g : Perm α} :
    support (g.extendDomain f) = g.support.map f.asEmbedding

Proof state:
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
rw [extendDomain_apply_subtype _ _ pb]

Result:
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Proof state:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
by_cases pb : p b

Result:
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Proof state:
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
simp only [not_exists, false_iff, not_and, eq_self_iff_true, not_true]

Result:
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ∀ (x : α), ¬g x = x → ¬f.asEmbedding x = b

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ f.asEmbedding (f.symm ⟨b, pb⟩) = b

Tactic:
simp

Result:
no goals

Proof state:
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b → ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
rintro h

Result:
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Proof state:
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
ha : ¬g a = a
hb : f.asEmbedding a = b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b

Tactic:
contrapose! ha

Result:
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : f.asEmbedding a = b
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ g a = a

Proof state:
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
constructor

Result:
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b → ∃ a, ¬g a = a ∧ f.asEmbedding a = b

case pos.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ (∃ a, ¬g a = a ∧ f.asEmbedding a = b) → ¬↑(f (g (f.symm ⟨b, pb⟩))) = b