case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
⊢ IsSwap f

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : IsSwap f
⊢ card (support f) = 2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 2 ↔ IsSwap f
constructor <;> intro h
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x : α
t : Finset α
hmem : ¬x ∈ t
hins : insert x t = support f
ht : card t = 1
⊢ IsSwap f
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
⊢ IsSwap f
obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x ∈ {y}
hins : {x, y} = support f
ht : card {y} = 1
⊢ IsSwap f
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x : α
t : Finset α
hmem : ¬x ∈ t
hins : insert x t = support f
ht : card t = 1
⊢ IsSwap f
obtain ⟨y, rfl⟩ := card_eq_one.1 ht
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
⊢ IsSwap f
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x ∈ {y}
hins : {x, y} = support f
ht : card {y} = 1
⊢ IsSwap f
rw [mem_singleton] at hmem
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
⊢ f = swap x y
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
⊢ IsSwap f
refine' ⟨x, y, hmem, _⟩
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
⊢ ↑f a = ↑(swap x y) a
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
⊢ f = swap x y
ext a
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
⊢ ↑f a = ↑(swap x y) a
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
⊢ ↑f a = ↑(swap x y) a
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ↑f a = a
⊢ ↑f a = ↑(swap x y) a

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ¬↑f a = a
⊢ ↑f a = ↑(swap x y) a
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
⊢ ↑f a = ↑(swap x y) a
by_cases ha : f a = a
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a b : α
⊢ ↑f b ≠ b ↔ ?m.185118 b
rw [← mem_support, ← hins, mem_insert, mem_singleton]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ↑f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ ↑f a = ↑(swap x y) a
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ↑f a = a
⊢ ↑f a = ↑(swap x y) a
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
no goals
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ↑f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ ↑f a = ↑(swap x y) a
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ¬↑f a = a
ha' : ↑f a = x ∨ ↑f a = y
⊢ ↑f a = ↑(swap x y) a
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ¬↑f a = a
⊢ ↑f a = ↑(swap x y) a
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
y : α
ht : card {y} = 1
a : α
ha : ¬↑f a = a
hmem : ¬a = y
hins : {a, y} = support f
key : ∀ (b : α), ↑f b ≠ b ↔ b = a ∨ b = y
ha' : ↑f a = a ∨ ↑f a = y
⊢ ↑f a = ↑(swap a y) a

case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x a : α
ha : ¬↑f a = a
hmem : ¬x = a
hins : {x, a} = support f
ht : card {a} = 1
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = a
ha' : ↑f a = x ∨ ↑f a = a
⊢ ↑f a = ↑(swap x a) a
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x y : α
hmem : ¬x = y
hins : {x, y} = support f
ht : card {y} = 1
a : α
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = y
ha : ¬↑f a = a
ha' : ↑f a = x ∨ ↑f a = y
⊢ ↑f a = ↑(swap x y) a
obtain rfl | rfl := (key a).mp ha
no goals
case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
y : α
ht : card {y} = 1
a : α
ha : ¬↑f a = a
hmem : ¬a = y
hins : {a, y} = support f
key : ∀ (b : α), ↑f b ≠ b ↔ b = a ∨ b = y
ha' : ↑f a = a ∨ ↑f a = y
⊢ ↑f a = ↑(swap a y) a
rw [Or.resolve_left ha' ha, swap_apply_left]
no goals
case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
x a : α
ha : ¬↑f a = a
hmem : ¬x = a
hins : {x, a} = support f
ht : card {a} = 1
key : ∀ (b : α), ↑f b ≠ b ↔ b = x ∨ b = a
ha' : ↑f a = x ∨ ↑f a = a
⊢ ↑f a = ↑(swap x a) a
rw [Or.resolve_right ha' ha, swap_apply_right]
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ card (support (swap x y)) = 2
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : IsSwap f
⊢ card (support f) = 2
obtain ⟨x, y, hxy, rfl⟩ := h
no goals
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ card (support (swap x y)) = 2
exact card_support_swap hxy