Theorem: Finperm.swap_mul_swap (Bruhat/Finperm.lean)

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ swap a b * swap a b = 1
Tactic:
obtain (rfl | hne) := eq_or_ne a b
State after:
case inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a : α
⊢ swap a a * swap a a = 1

case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ swap a b * swap a b = 1

State before:
case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ swap a b * swap a b = 1
Tactic:
apply funext_support_subset (s := {a,b})
State after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b * swap a b).support ⊆ {a, b}

case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ 1.support ⊆ {a, b}

case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ ∀ i ∈ {a, b}, (swap a b * swap a b) i = 1 i

State before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ ∀ i ∈ {a, b}, (swap a b * swap a b) i = 1 i
Tactic:
simp
State after:
no goals

State before:
case inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a : α
⊢ swap a a * swap a a = 1
Tactic:
simp [one_def]
State after:
no goals

State before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b * swap a b).support ⊆ {a, b}
Tactic:
refine (mul_support_subset _ _).trans ?_
State after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b).support ∪ (swap a b).support ⊆ {a, b}

State before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b).support ∪ (swap a b).support ⊆ {a, b}
Tactic:
rw [Finset.union_self, swap_support_of_ne hne]
State after:
no goals

State before:
case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ 1.support ⊆ {a, b}
Tactic:
simp
State after:
no goals