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

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ IsSwap (swap a b) ↔ a ≠ b
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ IsSwap (swap a b) → a ≠ b

case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ a ≠ b → IsSwap (swap a b)

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ IsSwap (swap a b) → a ≠ b
Tactic:
intro h hab
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ False
Tactic:
suffices Equiv.swap a b ≠ 1 by
  apply this
  rw [← hab, Equiv.swap_self]
  ext x; simp only [Equiv.coe_refl, Equiv.Perm.coe_one]
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ swap a b ≠ 1

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
⊢ swap a b ≠ 1
Tactic:
exact ne_one_of_isSwap h
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ False
Tactic:
apply this
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ swap a b = 1

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ swap a b = 1
Tactic:
rw [← hab, Equiv.swap_self]
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ Equiv.refl α = 1

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
⊢ Equiv.refl α = 1
Tactic:
ext x
State after:
case H
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
x : α
⊢ (Equiv.refl α) x = 1 x

State before:
case H
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : IsSwap (swap a b)
hab : a = b
this : swap a b ≠ 1
x : α
⊢ (Equiv.refl α) x = 1 x
Tactic:
simp only [Equiv.coe_refl, Equiv.Perm.coe_one]
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
⊢ a ≠ b → IsSwap (swap a b)
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ IsSwap (swap a b)

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ IsSwap (swap a b)
Tactic:
use a
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ ∃ y, a ≠ y ∧ swap a b = swap a y

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.15398
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
h : a ≠ b
⊢ ∃ y, a ≠ y ∧ swap a b = swap a y
Tactic:
use b
State after:
no goals