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

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
⊢ swap x y * swap y z * swap x y = swap x z
Tactic:
obtain (rfl | hxy) := eq_or_ne x y
State after:
case inl
α : Type u_1
x : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz hyz : x ≠ z
⊢ swap x x * swap x z * swap x x = swap x z

case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ swap x y * swap y z * swap x y = swap x z

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

case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x z).support ⊆ {x, y, z}

case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ ∀ i ∈ {x, y, z}, (swap x y * swap y z * swap x y) i = (swap x z) i

State before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ ∀ i ∈ {x, y, z}, (swap x y * swap y z * swap x y) i = (swap x z) i
Tactic:
simp only [mem_insert, mem_singleton, mul_apply, forall_eq_or_imp, swap_apply_left,
  swap_apply_right, forall_eq]
State after:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y) z = z ∧ (swap x y) ((swap y z) x) = (swap x z) y ∧ (swap x y) ((swap y z) ((swap x y) z)) = x

State before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y) z = z ∧ (swap x y) ((swap y z) x) = (swap x z) y ∧ (swap x y) ((swap y z) ((swap x y) z)) = x
Tactic:
rw [swap_apply_of_ne_of_ne hxz.symm hyz.symm, swap_apply_of_ne_of_ne hxy hxz,
  swap_apply_of_ne_of_ne hxy.symm hyz]
State after:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ z = z ∧ (swap x y) x = y ∧ (swap x y) ((swap y z) z) = x

State before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ z = z ∧ (swap x y) x = y ∧ (swap x y) ((swap y z) z) = x
Tactic:
simp
State after:
no goals

State before:
case inl
α : Type u_1
x : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz hyz : x ≠ z
⊢ swap x x * swap x z * swap x x = swap x z
Tactic:
simp
State after:
no goals

State before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y * swap y z * swap x y).support ⊆ {x, y, z}
Tactic:
rw [mul_support_eq, mul_support_eq]
State after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => (swap x y * swap y z) ((swap x y) x_1) ≠ x_1)
      (filter (fun x_1 => (swap x y) ((swap y z) x_1) ≠ x_1) ((swap x y).support ∪ (swap y z).support) ∪
        (swap x y).support) ⊆
    {x, y, z}

State before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => (swap x y * swap y z) ((swap x y) x_1) ≠ x_1)
      (filter (fun x_1 => (swap x y) ((swap y z) x_1) ≠ x_1) ((swap x y).support ∪ (swap y z).support) ∪
        (swap x y).support) ⊆
    {x, y, z}
Tactic:
simp only [mul_apply, ne_eq, swap_support, filter_congr_decidable, if_neg hxy, if_neg hyz]
State after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => ¬(swap x y) ((swap y z) ((swap x y) x_1)) = x_1)
      (filter (fun x_1 => ¬(swap x y) ((swap y z) x_1) = x_1) ({x, y} ∪ {y, z}) ∪ {x, y}) ⊆
    {x, y, z}

State before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => ¬(swap x y) ((swap y z) ((swap x y) x_1)) = x_1)
      (filter (fun x_1 => ¬(swap x y) ((swap y z) x_1) = x_1) ({x, y} ∪ {y, z}) ∪ {x, y}) ⊆
    {x, y, z}
Tactic:
refine (filter_subset _ _).trans (union_subset ((filter_subset _ _).trans ?_) (by aesop))
State after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ {x, y} ∪ {y, z} ⊆ {x, y, z}

State before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ {x, y} ∪ {y, z} ⊆ {x, y, z}
Tactic:
apply union_subset <;> aesop
State after:
no goals

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ {x, y} ⊆ {x, y, z}
Tactic:
aesop
State after:
no goals

State before:
case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x z).support ⊆ {x, y, z}
Tactic:
aesop
State after:
no goals