Theorem: Equiv.Perm.ne_one_of_isSwap (Jordan/PermMaximal.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
hf : IsSwap f
⊢ f ≠ 1
Tactic:
intro h1
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
hf : IsSwap f
h1 : f = 1
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
hf : IsSwap f
h1 : f = 1
⊢ False
Tactic:
obtain ⟨x, y, hxy, h⟩ := hf
State after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : f = swap x y
⊢ False

State before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : f = swap x y
⊢ False
Tactic:
rw [h1] at h
State after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ False

State before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ False
Tactic:
apply hxy
State after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = y

State before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = y
Tactic:
rw [← Equiv.swap_apply_left x y]
State after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = (swap x y) x

State before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = (swap x y) x
Tactic:
rw [← h]
State after:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = 1 x

State before:
case intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.14379
inst✝¹ : Group G
inst✝ : MulAction G α
f : Perm α
h1 : f = 1
x y : α
hxy : x ≠ y
h : 1 = swap x y
⊢ x = 1 x
Tactic:
simp only [Equiv.Perm.coe_one, id.def]
State after:
no goals