α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(↑f a = a ∨ ↑f b = b ∨ a = b)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ 1 < card (support f)
simp_rw [one_lt_card_iff, mem_support, ← not_or]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
⊢ f = 1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(↑f a = a ∨ ↑f b = b ∨ a = b)
contrapose! h
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
a : α
⊢ ↑f a = ↑1 a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
⊢ f = 1
ext a
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
a : α
h : ↑f (↑f a) = ↑f a ∨ ↑f a = a ∨ ↑f a = a
⊢ ↑f a = ↑1 a
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
a : α
⊢ ↑f a = ↑1 a
specialize h (f a) a
no goals
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
a : α
h : ↑f (↑f a) = ↑f a ∨ ↑f a = a ∨ ↑f a = a
⊢ ↑f a = ↑1 a
rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h