Theorem: Equiv.Perm.ofSubtype_eq_iff (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ ofSubtype (subtypePerm g hg) = c ↔
    support c ≤ s ∧ ∀ (hc' : ∀ (x : α), x ∈ s ↔ c x ∈ s), subtypePerm c hc' = subtypePerm g hg
Tactic:
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x) ↔
    support c ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x) ↔
    support c ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ (∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x) →
    support c ≤ 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
⊢ support c ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a) →
    ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x

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

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
⊢ support c ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)
Tactic:
suffices hc : support c ≤ s by
  use hc
  intro _ a ha
  rw [← h a, ofSubtype_apply_of_mem]
  rfl
  exact ha
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
⊢ support c ≤ s

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
⊢ support c ≤ s
Tactic:
intro a ha
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
a : α
ha : a ∈ support c
⊢ a ∈ s

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

State before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
a : α
ha : a ∈ support c
ha' : a ∉ s
⊢ False
Tactic:
rw [Equiv.Perm.mem_support, ← h a, ofSubtype_apply_of_not_mem] at ha
State after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
a : α
ha : a ≠ a
ha' : a ∉ s
⊢ False

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

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

case mp.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
a : α
ha : (ofSubtype (subtypePerm g hg)) a ≠ a
ha' : a ∉ s
⊢ a ∉ s
Tactic:
exact ha rfl
State after:
case mp.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
a : α
ha : (ofSubtype (subtypePerm g hg)) a ≠ a
ha' : a ∉ s
⊢ a ∉ s

State before:
case mp.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
a : α
ha : (ofSubtype (subtypePerm g hg)) a ≠ a
ha' : a ∉ s
⊢ a ∉ s
Tactic:
exact ha'
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
⊢ support c ≤ s ∧ ((∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a)
Tactic:
use hc
State after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
⊢ (∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
⊢ (∀ (x : α), x ∈ s ↔ c x ∈ s) → ∀ a ∈ s, c a = g a
Tactic:
intro _ a ha
State after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
hc'✝ : ∀ (x : α), x ∈ s ↔ c x ∈ s
a : α
ha : a ∈ s
⊢ c a = g a

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
hc'✝ : ∀ (x : α), x ∈ s ↔ c x ∈ s
a : α
ha : a ∈ s
⊢ c a = g a
Tactic:
rw [← h a, ofSubtype_apply_of_mem]
State after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
hc'✝ : ∀ (x : α), x ∈ s ↔ c x ∈ s
a : α
ha : a ∈ s
⊢ ↑((subtypePerm g hg) { val := a, property := ?right.ha }) = g a

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

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
hc'✝ : ∀ (x : α), x ∈ s ↔ c x ∈ s
a : α
ha : a ∈ s
⊢ ↑((subtypePerm g hg) { val := a, property := ?right.ha }) = g a

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

State before:
case right.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
h : ∀ (x : α), (ofSubtype (subtypePerm g hg)) x = c x
hc : support c ≤ s
hc'✝ : ∀ (x : α), x ∈ s ↔ c x ∈ s
a : α
ha : a ∈ s
⊢ a ∈ s
Tactic:
exact ha
State after:
no goals

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

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

State before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
⊢ (ofSubtype (subtypePerm g hg)) a = c a
Tactic:
by_cases ha : a ∈ s
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∈ s
⊢ (ofSubtype (subtypePerm g 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 : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ (ofSubtype (subtypePerm g hg)) a = c a

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∈ s
⊢ (ofSubtype (subtypePerm g hg)) a = c a
Tactic:
rw [h a ha, ofSubtype_apply_of_mem]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∈ s
⊢ ↑((subtypePerm g hg) { val := a, property := ?pos.ha✝ }) = g a

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

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∈ s
⊢ ↑((subtypePerm g hg) { val := a, property := ?pos.ha✝ }) = g a

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

State before:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∈ s
⊢ a ∈ s
Tactic:
exact ha
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ (ofSubtype (subtypePerm g hg)) a = c a
Tactic:
rw [ofSubtype_apply_of_not_mem]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a = c a

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

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

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

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

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

case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ support c

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

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

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

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

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

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

State before:
case neg.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), x ∈ s ↔ g x ∈ s
hc : support c ≤ s
a : α
h : ∀ a ∈ s, c a = g a
ha : a ∉ s
⊢ a ∉ s
Tactic:
exact ha
State after:
no goals