internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
⊢ Commute g c
Tactic:
ext x
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ (g * c) x = (c * g) x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ (g * c) x = (c * g) x
Tactic:
simp only [Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ g (c x) = c (g x)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
⊢ g (c x) = c (g x)
Tactic:
by_cases hx : x ∈ c.support
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c (g x)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g (c x) = c (g x)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c (g x)
Tactic:
rw [hi' x hx]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c ((c ^ i) x)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ g (c x) = c ((c ^ i) x)
Tactic:
rw [hi' (c x) (apply_mem_support.mpr hx)]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ i) (c x) = c ((c ^ i) x)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ i) (c x) = c ((c ^ i) x)
Tactic:
simp only [← Equiv.Perm.mul_apply, ← zpow_add_one, ← zpow_one_add]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ (i + 1)) x = (c ^ (1 + i)) x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∈ support c
⊢ (c ^ (i + 1)) x = (c ^ (1 + i)) x
Tactic:
rw [Int.add_comm 1 i]
Proof state after:
no goals
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g (c x) = c (g x)
Tactic:
rw [not_mem_support.mp hx]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g x = c (g x)
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g x = c (g x)
Tactic:
apply symm
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ c (g x) = g x
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ c (g x) = g x
Tactic:
rw [← Equiv.Perm.not_mem_support]
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g x ∉ support c
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
⊢ g x ∉ support c
Tactic:
intro hx'
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
hx' : g x ∈ support c
⊢ False
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
hx' : g x ∈ support c
⊢ False
Tactic:
apply hx
Proof state after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
hx' : g x ∈ support c
⊢ x ∈ support c
Theorem: Equiv.Perm.IsCycle.commute_iff'
Proof state before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : IsCycle c
hc' : ∀ (x : α), x ∈ support c ↔ g x ∈ support c
i : ℤ
hi : (fun x => subtypePermOfSupport c ^ x) i = subtypePerm g hc'
hi' : ∀ x ∈ support c, g x = (c ^ i) x
x : α
hx : x ∉ support c
hx' : g x ∈ support c
⊢ x ∈ support c
Tactic:
exact (hc' x).mpr hx'
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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]
Proof 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)
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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)
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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'
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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'
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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)
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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]
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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
Proof 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
Theorem: Equiv.Perm.ofSubtype_eq_iff
Proof 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]
Proof 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