-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_eq_two {f : Perm α} : #f.support = 2 ↔ IsSwap f

Proof state:
case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : #{y} = 1
a : α
ha : ¬f a = a
hmem : ¬a = y
hins : {a, y} = f.support
key : ∀ (b : α), f b ≠ b ↔ b = a ∨ b = y
ha' : f a = a ∨ f a = y
⊢ f a = (swap a y) a

Tactic:
rw [Or.resolve_left ha' ha, swap_apply_left]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : x ∉ {y}
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f.IsSwap

Tactic:
rw [mem_singleton] at hmem

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f.IsSwap

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
⊢ f a = (swap x y) a

Tactic:
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{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

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
⊢ f.IsSwap

Tactic:
obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h

Result:
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x : α
t : Finset α
hmem : x ∉ t
hins : insert x t = f.support
ht : #t = 1
⊢ f.IsSwap

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ #(swap x y).support = 2

Tactic:
exact card_support_swap hxy

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x : α
t : Finset α
hmem : x ∉ t
hins : insert x t = f.support
ht : #t = 1
⊢ f.IsSwap

Tactic:
obtain ⟨y, rfl⟩ := card_eq_one.1 ht

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : x ∉ {y}
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f.IsSwap

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 2 ↔ f.IsSwap

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
⊢ f.IsSwap

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f = swap x y

Tactic:
ext a

Result:
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
⊢ f a = (swap x y) a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a b : α
⊢ f b ≠ b ↔ ?m.79587 b

Tactic:
rw [← mem_support, ← hins, mem_insert, mem_singleton]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
⊢ f a = (swap x y) a

Tactic:
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]

Result:
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
⊢ f a = (swap x y) a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f.IsSwap

Tactic:
refine ⟨x, y, hmem, ?_⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f = swap x y

Proof state:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2

Tactic:
obtain ⟨x, y, hxy, rfl⟩ := h

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ #(swap x y).support = 2

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{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

Tactic:
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : ¬f a = a
⊢ f a = (swap x y) a

Tactic:
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{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

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{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

Tactic:
obtain rfl | rfl := (key a).mp ha

Result:
case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : #{y} = 1
a : α
ha : ¬f a = a
hmem : ¬a = y
hins : {a, y} = f.support
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 : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ f a = (swap x a) a

Proof state:
case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ f a = (swap x a) a

Tactic:
rw [Or.resolve_right ha' ha, swap_apply_right]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
⊢ f a = (swap x y) a

Tactic:
by_cases ha : f a = a

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{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 : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : ¬f a = a
⊢ f a = (swap x y) a