-- Mathlib/GroupTheory/Perm/Support.lean
/-- A permutation c is the extension of a restriction of g to s
  iff its support is contained in s and its restriction is that of g -/
lemma ofSubtype_eq_iff {g c : Equiv.Perm α} {s : Finset α}
    (hg : ∀ x, x ∈ s ↔ g x ∈ s) :
    ofSubtype (g.subtypePerm hg) = c ↔
      c.support ≤ s ∧
      ∀ (hc' : ∀ x, x ∈ s ↔ c x ∈ s), c.subtypePerm hc' = g.subtypePerm hg

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
h : (∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a
a : α
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Tactic:
specialize h (isInvariant_of_support_le hc)

Result:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
a : α
h : ∀ a ∈ s, c a = g a
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
a : α
h : ∀ a ∈ s, c a = g a
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Tactic:
by_cases ha : a ∈ s

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) →
    c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ c.support

Tactic:
exact Finset.not_mem_mono hc ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ ofSubtype (g.subtypePerm hg) = c ↔
    c.support ≤ s ∧ ∀ (hc' : ∀ (x : α), x ∈ s ↔ c x ∈ s), c.subtypePerm hc' = g.subtypePerm hg

Tactic:
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) ↔
    c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

Proof state:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ (∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a

Tactic:
intro _ a ha

Result:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), x ∈ s ↔ c x ∈ s
a : α
ha : a ∈ s
⊢ c a = g a

Proof state:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ≠ a
ha' : a ∉ s
⊢ False

Tactic:
exact ha rfl

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a) →
    ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x

Tactic:
rintro ⟨hc, h⟩ a

Result:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : c.support ≤ s
h : (∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a
a : α
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Proof state:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ≤ s

Tactic:
intro a ha

Result:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ∈ c.support
⊢ a ∈ s

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) ↔
    c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) →
    c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a) →
    ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x

Proof state:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ∈ c.support
⊢ a ∈ s

Tactic:
by_contra ha'

Result:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : a ∈ c.support
ha' : a ∉ s
⊢ False

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

Tactic:
constructor

Result:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ≤ s

case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ (∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a