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

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
⊢ (f * swap x (f⁻¹ x)).support ⊆ erase f.support x
Tactic:
intro y hy
State after:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ y ∈ erase f.support x

State before:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ y ∈ erase f.support x
Tactic:
simp only [mem_erase, ne_eq, mem_support_iff]
State after:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ ¬y = x ∧ ¬f y = y

State before:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ ¬y = x ∧ ¬f y = y
Tactic:
obtain (rfl | hne) := eq_or_ne y x
State after:
case inl
α : Type u_1
y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
y : α
hx : y ∈ f.support
hy : y ∈ (f * swap y (f⁻¹ y)).support
⊢ ¬y = y ∧ ¬f y = y

case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
⊢ ¬y = x ∧ ¬f y = y

State before:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
⊢ ¬y = x ∧ ¬f y = y
Tactic:
refine ⟨hne, fun hy' ↦ ?_⟩
State after:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
hy' : f y = y
⊢ False

State before:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
hy' : f y = y
⊢ False
Tactic:
simp only [mem_support_iff, mul_apply, ne_eq] at hy
State after:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
⊢ False

State before:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
⊢ False
Tactic:
obtain (rfl | hne') := eq_or_ne y (f⁻¹ x)
State after:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy' : f (f⁻¹ x) = f⁻¹ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
⊢ False

case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
hne' : y ≠ f⁻¹ x
⊢ False

State before:
case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
hne' : y ≠ f⁻¹ x
⊢ False
Tactic:
rw [swap_apply_of_ne_of_ne hne hne'] at hy
State after:
case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f y = y
hne' : y ≠ f⁻¹ x
⊢ False

State before:
case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f y = y
hne' : y ≠ f⁻¹ x
⊢ False
Tactic:
exact hy hy'
State after:
no goals

State before:
case inl
α : Type u_1
y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
y : α
hx : y ∈ f.support
hy : y ∈ (f * swap y (f⁻¹ y)).support
⊢ ¬y = y ∧ ¬f y = y
Tactic:
simp at hy
State after:
no goals

State before:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy' : f (f⁻¹ x) = f⁻¹ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
⊢ False
Tactic:
simp only [swap_apply_right, apply_inv_apply] at hy'
State after:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False

State before:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False
Tactic:
rw [← hy'] at hne
State after:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False

State before:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False
Tactic:
exact hne rfl
State after:
no goals