-- 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.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
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
hb : f.asEmbedding (f.symm ⟨b, pb⟩) = b
⊢ g (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩

Tactic:
rw [eq_symm_apply]

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
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
hb : f.asEmbedding (f.symm ⟨b, pb⟩) = b
⊢ f (g (f.symm ⟨b, pb⟩)) = ⟨b, pb⟩

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
⊢ ∀ (x : α), ¬g x = x → ¬f.asEmbedding x = b

Tactic:
rintro a _ rfl

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 α
a : α
a✝ : ¬g a = a
pb : ¬p (f.asEmbedding a)
⊢ False

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
h : ¬↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
refine ⟨f.symm ⟨b, pb⟩, ?_, by simp⟩

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
⊢ ¬g (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩

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
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
hb : f.asEmbedding (f.symm ⟨b, pb⟩) = b
⊢ f (g (f.symm ⟨b, pb⟩)) = ⟨b, pb⟩

Tactic:
exact Subtype.coe_injective ha

Result:
no goals

Proof state:
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

Tactic:
rintro ⟨a, ha, hb⟩

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 : α
ha : ¬g a = a
hb : f.asEmbedding a = b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = 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
a : α
hb : f.asEmbedding a = b
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ a = f.symm ⟨b, pb⟩

Tactic:
rw [eq_symm_apply]

Result:
α : 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
⊢ f a = ⟨b, pb⟩

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 : β
⊢ b ∈ (g.extendDomain f).support ↔ b ∈ map f.asEmbedding g.support

Tactic:
simp only [exists_prop, Function.Embedding.coeFn_mk, toEmbedding_apply, mem_map, Ne,
  Function.Embedding.trans_apply, mem_support]

Result:
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

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 : α
hb : f.asEmbedding a = b
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ g a = a

Tactic:
obtain rfl : a = f.symm ⟨b, pb⟩ := by
  rw [eq_symm_apply]
  exact Subtype.coe_injective hb

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
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
hb : f.asEmbedding (f.symm ⟨b, pb⟩) = b
⊢ g (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩

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 α
a : α
a✝ : ¬g a = a
pb : ¬p (f.asEmbedding a)
⊢ False

Tactic:
exact pb (Subtype.prop _)

Result:
no goals

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
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
rw [extendDomain_apply_not_subtype _ _ pb]

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
⊢ ¬b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

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
h : ¬↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ ¬g (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩

Tactic:
contrapose! 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 : g (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩
⊢ ↑(f (g (f.symm ⟨b, pb⟩))) = b

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
h : g (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩
⊢ ↑(f (g (f.symm ⟨b, pb⟩))) = b

Tactic:
simp [h]

Result:
no goals

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 α
⊢ (g.extendDomain f).support = map f.asEmbedding g.support

Tactic:
ext b

Result:
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 : β
⊢ b ∈ (g.extendDomain f).support ↔ b ∈ map f.asEmbedding g.support

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
a : α
hb : f.asEmbedding a = b
ha : ↑(f (g (f.symm ⟨b, pb⟩))) = b
⊢ f a = ⟨b, pb⟩

Tactic:
exact Subtype.coe_injective hb

Result:
no goals