[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f g → Disjoint g f
[PROOFSTEP]
simp only [Disjoint, or_comm, imp_self]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hf : ↑f x = x
hg : ↑f (↑g x) = ↑g x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, hf, hg]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hf : ↑f x = x
hg : ↑g (↑g x) = ↑g x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, hf, g.injective hg]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hg : ↑g x = x
hf : ↑f (↑f x) = ↑f x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, f.injective hf, hg]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
hg : ↑g x = x
hf : ↑g (↑f x) = ↑f x
⊢ ↑(f * g) x = ↑(g * f) x
[PROOFSTEP]
simp [mul_apply, hf, hg]
[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f f ↔ f = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ disjoint_one_left 1⟩
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
⊢ f = 1
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
⊢ ↑f x = ↑1 x
[PROOFSTEP]
cases' h x with hx hx
[GOAL]
case H.inl
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
hx : ↑f x = x
⊢ ↑f x = ↑1 x
[PROOFSTEP]
simp [hx]
[GOAL]
case H.inr
α : Type u_1
f g h✝ : Perm α
h : Disjoint f f
x : α
hx : ↑f x = x
⊢ ↑f x = ↑1 x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
⊢ Disjoint f⁻¹ g
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f⁻¹ x = x ∨ ↑g x = x
[PROOFSTEP]
rw [inv_eq_iff_eq, eq_comm]
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f g
x : α
⊢ ↑f x = x ∨ ↑g x = x
[PROOFSTEP]
exact h x
[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f⁻¹ g ↔ Disjoint f g
[PROOFSTEP]
refine' ⟨fun h => _, Disjoint.inv_left⟩
[GOAL]
α : Type u_1
f g h✝ : Perm α
h : Disjoint f⁻¹ g
⊢ Disjoint f g
[PROOFSTEP]
convert h.inv_left
[GOAL]
α : Type u_1
f g h : Perm α
⊢ Disjoint f g⁻¹ ↔ Disjoint f g
[PROOFSTEP]
rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]
[GOAL]
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
cases H1 x
[GOAL]
case inl
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝ : ↑f x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
cases H2 x
[GOAL]
case inr
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝ : ↑h x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
cases H2 x
[GOAL]
case inl.inl
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ : ↑f x = x
h✝ : ↑g x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
case inl.inr
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ : ↑f x = x
h✝ : ↑h x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inl
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ : ↑h x = x
h✝ : ↑g x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
case inr.inr
α : Type u_1
f g h : Perm α
H1 : Disjoint f h
H2 : Disjoint g h
x : α
h✝¹ h✝ : ↑h x = x
⊢ ↑(f * g) x = x ∨ ↑h x = x
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint f (g * h)
[PROOFSTEP]
rw [disjoint_comm]
[GOAL]
α : Type u_1
f g h : Perm α
H1 : Disjoint f g
H2 : Disjoint f h
⊢ Disjoint (g * h) f
[PROOFSTEP]
exact H1.symm.mul_left H2.symm
[GOAL]
α : Type u_1
f g h✝ h : Perm α
x✝ : α
⊢ ↑(h * f * h⁻¹) x✝ = x✝ ∨ ↑(h * g * h⁻¹) x✝ = x✝ ↔ ↑f (↑h⁻¹ x✝) = ↑h⁻¹ x✝ ∨ ↑g (↑h⁻¹ x✝) = ↑h⁻¹ x✝
[PROOFSTEP]
simp only [mul_apply, eq_inv_iff_eq]
[GOAL]
α : Type u_1
f g h✝ : Perm α
l : List (Perm α)
h : ∀ (g : Perm α), g ∈ l → Disjoint f g
⊢ Disjoint f (List.prod l)
[PROOFSTEP]
induction' l with g l ih
[GOAL]
case nil
α : Type u_1
f g h✝¹ : Perm α
l : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l → Disjoint f g
h : ∀ (g : Perm α), g ∈ [] → Disjoint f g
⊢ Disjoint f (List.prod [])
[PROOFSTEP]
exact disjoint_one_right _
[GOAL]
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (List.prod (g :: l))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (g * List.prod l)
[PROOFSTEP]
exact (h _ (List.mem_cons_self _ _)).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ List.Nodup l
[PROOFSTEP]
refine' List.Pairwise.imp_of_mem _ h2
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
⊢ ∀ {a b : Perm α}, a ∈ l → b ∈ l → Disjoint a b → a ≠ b
[PROOFSTEP]
intro τ σ h_mem _ h_disjoint _
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
τ σ : Perm α
h_mem : τ ∈ l
a✝¹ : σ ∈ l
h_disjoint : Disjoint τ σ
a✝ : τ = σ
⊢ False
[PROOFSTEP]
subst τ
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ False
[PROOFSTEP]
suffices (σ : Perm α) = 1 by
  rw [this] at h_mem 
  exact h1 h_mem
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
[PROOFSTEP]
rw [this] at h_mem 
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ : σ ∈ l
h_mem : 1 ∈ l
h_disjoint : Disjoint σ σ
this : σ = 1
⊢ False
[PROOFSTEP]
exact h1 h_mem
[GOAL]
α : Type u_1
f g h : Perm α
l : List (Perm α)
h1 : ¬1 ∈ l
h2 : List.Pairwise Disjoint l
σ : Perm α
a✝ h_mem : σ ∈ l
h_disjoint : Disjoint σ σ
⊢ σ = 1
[PROOFSTEP]
exact ext fun a => (or_self_iff _).mp (h_disjoint a)
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hfx : ↑f x = x
n : ℕ
⊢ ↑(f ^ (n + 1)) x = x
[PROOFSTEP]
rw [pow_succ', mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hfx : ↑f x = x
n : ℕ
⊢ ↑(f ^ Int.negSucc n) x = x
[PROOFSTEP]
rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
[GOAL]
α : Type u_1
f g h✝ : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
h : ↑(f ^ n) x = x
⊢ ↑(f ^ (n + 1)) x = ↑f x
[PROOFSTEP]
rw [pow_succ, mul_apply, h]
[GOAL]
α : Type u_1
f g h✝ : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
h : ↑(f ^ n) x = ↑f x
⊢ ↑(f ^ (n + 1)) x = x
[PROOFSTEP]
rw [pow_succ, mul_apply, h, hffx]
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ Int.negSucc n) x = x ∨ ↑(f ^ Int.negSucc n) x = ↑f x
[PROOFSTEP]
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ, eq_comm, inv_eq_iff_eq, ← mul_apply, ←
  pow_succ', @eq_comm _ x, or_comm]
[GOAL]
α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ (n + 1 + 1)) x = x ∨ ↑(f ^ (n + 1 + 1)) x = ↑f x
[PROOFSTEP]
exact pow_apply_eq_of_apply_apply_eq_self hffx _
[GOAL]
α : Type u_1
f g h σ τ : Perm α
hστ : Disjoint σ τ
a : α
⊢ ↑(σ * τ) a = a ↔ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [mul_apply, h.2, h.1]⟩
[GOAL]
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑σ a = a ∧ ↑τ a = a
⊢ ↑(σ * τ) a = a
[PROOFSTEP]
rw [mul_apply, h.2, h.1]
[GOAL]
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
⊢ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
cases' hστ a with hσ hτ
[GOAL]
case inl
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hσ : ↑σ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩
[GOAL]
case inr
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hτ : ↑τ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
[PROOFSTEP]
exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩
[GOAL]
α : Type u_1
f g h σ τ : Perm α
hστ : Disjoint σ τ
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1
[PROOFSTEP]
simp_rw [ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
⊢ ↑(↑ofSubtype (swap x y)) z = ↑(swap ↑x ↑y) z
[PROOFSTEP]
by_cases hz : p z
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ ↑(↑ofSubtype (swap x y)) z = ↑(swap ↑x ↑y) z
[PROOFSTEP]
rw [swap_apply_def, ofSubtype_apply_of_mem _ hz]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
⊢ ↑(↑(swap x y) { val := z, property := hz }) = if z = ↑x then ↑y else if z = ↑y then ↑x else z
[PROOFSTEP]
split_ifs with hzx hzy
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : z = ↑x
⊢ ↑(↑(swap x y) { val := z, property := hz }) = ↑y
[PROOFSTEP]
simp_rw [hzx, Subtype.coe_eta, swap_apply_left]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : z = ↑y
⊢ ↑(↑(swap x y) { val := z, property := hz }) = ↑x
[PROOFSTEP]
simp_rw [hzy, Subtype.coe_eta, swap_apply_right]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ ↑(↑(swap x y) { val := z, property := hz }) = z
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ { val := z, property := hz } ≠ x
[PROOFSTEP]
simp [Subtype.ext_iff, *]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : p z
hzx : ¬z = ↑x
hzy : ¬z = ↑y
⊢ { val := z, property := hz } ≠ y
[PROOFSTEP]
simp [Subtype.ext_iff, *]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ ↑(↑ofSubtype (swap x y)) z = ↑(swap ↑x ↑y) z
[PROOFSTEP]
rw [ofSubtype_apply_of_not_mem _ hz, swap_apply_of_ne_of_ne]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑x
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
intro h
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ False
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
apply hz
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p z
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
rw [h]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑x
⊢ p ↑x
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
exact Subtype.prop x
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
⊢ z ≠ ↑y
[PROOFSTEP]
intro h
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ False
[PROOFSTEP]
apply hz
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p z
[PROOFSTEP]
rw [h]
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
z : α
hz : ¬p z
h : z = ↑y
⊢ p ↑y
[PROOFSTEP]
exact Subtype.prop y
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : IsSwap f
x : α
hx : p x
y : α
hy : p y
hxy :
  { val := x, property := hx } ≠ { val := y, property := hy } ∧
    f = swap { val := x, property := hx } { val := y, property := hy }
⊢ x ≠ y
[PROOFSTEP]
simp only [Ne.def, Subtype.ext_iff] at hxy 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : IsSwap f
x : α
hx : p x
y : α
hy : p y
hxy : ¬x = y ∧ f = swap { val := x, property := hx } { val := y, property := hy }
⊢ x ≠ y
[PROOFSTEP]
exact hxy.1
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : IsSwap f
x : α
hx : p x
y : α
hy : p y
hxy :
  { val := x, property := hx } ≠ { val := y, property := hy } ∧
    f = swap { val := x, property := hx } { val := y, property := hy }
⊢ ↑ofSubtype f = swap x y
[PROOFSTEP]
rw [hxy.2, ofSubtype_swap_eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : ↑(swap x (↑f x) * f) y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
by_cases h : f y = x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
constructor
[GOAL]
case pos.left
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y
[PROOFSTEP]
intro
[GOAL]
case pos.right
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ y ≠ x
[PROOFSTEP]
intro
[GOAL]
case pos.left
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : ↑f y = y
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case pos.right
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : y = x
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ¬↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
split_ifs at hy  with h h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{subst x
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
subst x
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {subst x
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{subst x
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬↑f y = x
h : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp [*] at *
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{simp [*] at *
}
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp [*] at *
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
try {simp [*] at *
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
{simp [*] at *
}
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝¹ : ¬↑f y = x
h✝ : ¬↑f y = x
h : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp [*] at *
[GOAL]
α : Type u_1
p q : Perm α
⊢ {x | ↑p⁻¹ x ≠ x} = {x | ↑p x ≠ x}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑p⁻¹ x ≠ x} ↔ x ∈ {x | ↑p x ≠ x}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Ne.def]
[GOAL]
case h
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p⁻¹ x = x ↔ ¬↑p x = x
[PROOFSTEP]
rw [inv_def, symm_apply_eq, eq_comm]
[GOAL]
α : Type u_1
p✝ q p : Perm α
a : α
⊢ ↑p a ∈ {x | ↑p x ≠ x} ↔ a ∈ {x | ↑p x ≠ x}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
⊢ {x | ↑(p ^ n) x ≠ x} ⊆ {x | ↑p x ≠ x}
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ x ∈ {x | ↑(p ^ n) x ≠ x} → x ∈ {x | ↑p x ≠ x}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Ne.def]
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
x : α
⊢ ¬↑(p ^ n) x = x → ¬↑p x = x
[PROOFSTEP]
intro hx H
[GOAL]
α : Type u_1
p q : Perm α
n : ℤ
x : α
hx : ¬↑(p ^ n) x = x
H : ↑p x = x
⊢ False
[PROOFSTEP]
simp [zpow_apply_eq_self_of_apply_eq_self H] at hx 
[GOAL]
α : Type u_1
p q : Perm α
⊢ {x | ↑(p * q) x ≠ x} ⊆ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | ↑(p * q) x ≠ x} → x ∈ {x | ↑p x ≠ x} ∪ {x | ↑q x ≠ x}
[PROOFSTEP]
simp only [Perm.coe_mul, Function.comp_apply, Ne.def, Set.mem_union, Set.mem_setOf_eq]
[GOAL]
α : Type u_1
p q : Perm α
x : α
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
[PROOFSTEP]
by_cases hq : q x = x
[GOAL]
case pos
α : Type u_1
p q : Perm α
x : α
hq : ↑q x = x
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
α : Type u_1
p q : Perm α
x : α
hq : ¬↑q x = x
⊢ ¬↑p (↑q x) = x → ¬↑p x = x ∨ ¬↑q x = x
[PROOFSTEP]
simp [hq]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ support f ↔ ↑f x ≠ x
[PROOFSTEP]
rw [support, mem_filter, and_iff_right (mem_univ x)]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ ¬x ∈ support f ↔ ↑f x = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ ↑(support f) = {x | ↑f x ≠ x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x✝ : α
⊢ x✝ ∈ ↑(support f) ↔ x✝ ∈ {x | ↑f x ≠ x}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g σ : Perm α
⊢ support σ = ∅ ↔ σ = 1
[PROOFSTEP]
simp_rw [Finset.ext_iff, mem_support, Finset.not_mem_empty, iff_false_iff, not_not, Equiv.Perm.ext_iff, one_apply]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ support 1 = ∅
[PROOFSTEP]
rw [support_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
by_cases hx : x ∈ g.support
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : x ∈ support g
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact h' x hx
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [not_mem_support.mp hx, ← not_mem_support]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : support f ⊆ support g
h' : ∀ (x : α), x ∈ support g → ↑f x = ↑g x
x : α
hx : ¬x ∈ support g
⊢ ¬x ∈ support f
[PROOFSTEP]
exact fun H => hx (h H)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ⊔ support g
[PROOFSTEP]
simp only [sup_eq_union]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ x ∈ support (f * g) → x ∈ support f ∪ support g
[PROOFSTEP]
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
⊢ ↑f x = x ∧ ↑g x = x → ↑f (↑g x) = x
[PROOFSTEP]
rintro ⟨hf, hg⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g✝ f g : Perm α
x : α
hf : ↑f x = x
hg : ↑g x = x
⊢ ↑f (↑g x) = x
[PROOFSTEP]
rw [hg, hf]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : x ∈ support (List.prod l)
⊢ ∃ f, f ∈ l ∧ x ∈ support f
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ¬x ∈ support f
⊢ ¬x ∈ support (List.prod l)
[PROOFSTEP]
simp_rw [mem_support, not_not] at hx ⊢
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ↑f x = x
⊢ ↑(List.prod l) x = x
[PROOFSTEP]
induction' l with f l ih
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l → ↑f x = x
hx : ∀ (f : Perm α), f ∈ [] → ↑f x = x
⊢ ↑(List.prod []) x = x
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ↑(List.prod (f :: l)) x = x
[PROOFSTEP]
rw [List.prod_cons, mul_apply, ih, hx]
[GOAL]
case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ f ∈ f :: l
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
[PROOFSTEP]
simp only [List.find?, List.mem_cons, true_or]
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
[PROOFSTEP]
intros f' hf'
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ ↑f' x = x
[PROOFSTEP]
refine' hx f' _
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' ∈ f :: l
[PROOFSTEP]
simp only [List.find?, List.mem_cons]
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' = f ∨ f' ∈ l
[PROOFSTEP]
exact Or.inr hf'
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g σ : Perm α
⊢ support σ⁻¹ = support σ
[PROOFSTEP]
simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ ↑f x ∈ support f ↔ x ∈ support f
[PROOFSTEP]
rw [mem_support, mem_support, Ne.def, Ne.def, apply_eq_iff_eq]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
n : ℕ
x : α
⊢ ↑f (↑(f ^ n) x) = ↑(f ^ n) x ↔ ↑f x = x
[PROOFSTEP]
rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]
  -- @[simp] -- Porting note: simp can prove this
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
n : ℕ
x : α
⊢ ↑(f ^ n) x ∈ support f ↔ x ∈ support f
[PROOFSTEP]
simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
n : ℤ
x : α
⊢ ↑f (↑(f ^ n) x) = ↑(f ^ n) x ↔ ↑f x = x
[PROOFSTEP]
rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]
  -- @[simp] -- Porting note: simp can prove this
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
n : ℤ
x : α
⊢ ↑(f ^ n) x ∈ support f ↔ x ∈ support f
[PROOFSTEP]
simp only [mem_support, ne_eq, apply_zpow_apply_eq_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.zero) x = ↑(g ^ Nat.zero) x
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
[PROOFSTEP]
intro x hx
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
[PROOFSTEP]
rw [pow_succ', mul_apply, pow_succ', mul_apply, h _ hx, hk]
[GOAL]
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑g x ∈ support f ∩ support g
[PROOFSTEP]
rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ Disjoint f g ↔ _root_.Disjoint (support f) (support g)
[PROOFSTEP]
simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff, not_and_or, imp_iff_not_or]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ support (f * g) = support f ∪ support g
[PROOFSTEP]
refine' le_antisymm (support_mul_le _ _) fun a => _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ a ∈ support f ∪ support g → a ∈ support (f * g)
[PROOFSTEP]
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a : α
⊢ ↑f (↑g a) = a → ↑f a = a ∧ ↑g a = a
[PROOFSTEP]
exact
  (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h => ⟨(congr_arg f hg).symm.trans h, hg⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ support (List.prod l) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support l)
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
h : List.Pairwise Disjoint []
⊢ support (List.prod []) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
rw [List.pairwise_cons] at h 
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → support (List.prod tl) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
h : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
this : Disjoint hd (List.prod tl)
⊢ support (List.prod (hd :: tl)) = List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
simp [this.support_mul, hl h.right]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
⊢ support (List.prod l) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support l)
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ support (List.prod []) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (List.prod (hd :: tl)) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.foldr_cons]
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support (hd * List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
[PROOFSTEP]
refine' (support_mul_le hd tl.prod).trans _
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g hd : Perm α
tl : List (Perm α)
hl : support (List.prod tl) ≤ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
⊢ support hd ⊔ support (List.prod tl) ≤ support hd ⊔ List.foldr (fun x x_1 => x ⊔ x_1) ⊥ (List.map support tl)
[PROOFSTEP]
exact sup_le_sup le_rfl hl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
⊢ support (swap x y) = {x, y}
[PROOFSTEP]
ext z
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
by_cases hx : z = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
any_goals simpa [hx] using h.symm
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simpa [hx] using h.symm
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simpa [hx] using h.symm
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
by_cases hy : z = y
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : z = y
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, hx, hy]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : z = y
⊢ ¬x = y
[PROOFSTEP]
exact h
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : ¬z = y
⊢ z ∈ support (swap x y) ↔ z ∈ {x, y}
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, hx, hy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ support (swap x y) = {x, y} ↔ x ≠ y
[PROOFSTEP]
refine' ⟨fun h => _, fun h => support_swap h⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
⊢ x ≠ y
[PROOFSTEP]
by_contra'
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x y) = {x, y}
this : x = y
⊢ False
[PROOFSTEP]
rw [← this] at h 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : support (swap x x) = {x, x}
this : x = y
⊢ False
[PROOFSTEP]
simp only [swap_self, support_refl, pair_eq_singleton] at h 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ False
[PROOFSTEP]
have : x ∈ ∅ := by
  rw [h]
  exact mem_singleton.mpr rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ ∅
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ x ∈ {x}
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this : x = y
h : ∅ = {x}
⊢ Membership α (Finset α)
[PROOFSTEP]
exact mem_singleton.mpr rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝ : x = y
h : ∅ = {x}
this : x ∈ ∅
⊢ False
[PROOFSTEP]
have := (Finset.ne_empty_of_mem this)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
this✝¹ : x = y
h : ∅ = {x}
this✝ : x ∈ ∅
this : ∅ ≠ ∅
⊢ False
[PROOFSTEP]
exact this rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : List.Nodup [x, y, z]
⊢ support (swap x y * swap y z) = {x, y, z}
[PROOFSTEP]
simp only [List.not_mem_nil, and_true_iff, List.mem_cons, not_false_iff, List.nodup_cons, List.mem_singleton,
  and_self_iff, List.nodup_nil] at h 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ support (swap x y * swap y z) = {x, y, z}
[PROOFSTEP]
push_neg at h 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) = {x, y, z}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ support (swap x y * swap y z) ≤ {x, y, z}
[PROOFSTEP]
convert support_mul_le (swap x y) (swap y z) using 1
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = support (swap x y) ⊔ support (swap y z)
[PROOFSTEP]
rw [support_swap h.left.left, support_swap h.right.left]
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ⊔ {y, z}
[PROOFSTEP]
simp only [sup_eq_union]
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = {x, y} ∪ {y, z}
[PROOFSTEP]
simp only [mem_singleton, mem_insert, union_insert, insert_union, mem_union, true_or, or_true, insert_eq_of_mem]
[GOAL]
case h.e'_4
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} = insert x ({y} ∪ {z})
[PROOFSTEP]
rfl
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ {x, y, z} ≤ support (swap x y * swap y z)
[PROOFSTEP]
intro
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ ∈ {x, y, z} → a✝ ∈ support (swap x y * swap y z)
[PROOFSTEP]
simp only [mem_insert, mem_singleton]
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
a✝ : α
⊢ a✝ = x ∨ a✝ = y ∨ a✝ = z → a✝ ∈ support (swap x y * swap y z)
[PROOFSTEP]
rintro (rfl | rfl | rfl | _)
[GOAL]
case a.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
y z a✝ : α
h : (a✝ ≠ y ∧ a✝ ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ a✝ ∈ support (swap a✝ y * swap y z)
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
  h.right.left.symm]
[GOAL]
case a.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x z a✝ : α
h : (x ≠ a✝ ∧ x ≠ z ∧ ¬False) ∧ a✝ ≠ z ∧ ¬False
⊢ a✝ ∈ support (swap x a✝ * swap a✝ z)
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
  h.right.left.symm]
[GOAL]
case a.inr.inr.refl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False
⊢ z ∈ support (swap x y * swap y z)
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
  h.right.left.symm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y : α
⊢ support f \ {x, y} ≤ support (swap x y * f)
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ a✝ ∈ support f \ {x, y} → a✝ ∈ support (swap x y * f)
[PROOFSTEP]
simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne.def, mem_support, mem_insert, mem_sdiff, mem_singleton]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ¬↑f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬↑(swap x y) (↑f a✝) = a✝
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
⊢ ↑f a✝ ≠ a✝ → a✝ ≠ x ∧ a✝ ≠ y → ↑(swap x y) (↑f a✝) ≠ a✝
[PROOFSTEP]
rintro ha ⟨hx, hy⟩ H
[GOAL]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑(swap x y) (↑f a✝) = a✝
⊢ False
[PROOFSTEP]
rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H 
[GOAL]
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x y a✝ : α
ha : ↑f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : ↑f a✝ = a✝
⊢ False
[PROOFSTEP]
exact ha H
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
⊢ support (swap x (↑f x) * f) = support f \ {x}
[PROOFSTEP]
by_cases hx : f x = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ↑f x = x
⊢ support (swap x (↑f x) * f) = support f \ {x}
[PROOFSTEP]
simp [hx, sdiff_singleton_eq_erase, not_mem_support.mpr hx, erase_eq_of_not_mem]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
⊢ support (swap x (↑f x) * f) = support f \ {x}
[PROOFSTEP]
ext z
[GOAL]
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
by_cases hzx : z = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [hzx]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
by_cases hzf : z = f x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [hzf, hx, h, swap_apply_of_ne_of_ne]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
by_cases hzfx : f z = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
h : ↑f (↑f x) ≠ x
hx : ¬↑f x = x
z : α
hzx : ¬z = x
hzf : ¬z = ↑f x
hzfx : ¬↑f z = x
⊢ z ∈ support (swap x (↑f x) * f) ↔ z ∈ support f \ {x}
[PROOFSTEP]
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : y ∈ support (swap x (↑f x) * f)
⊢ y ∈ support f ∧ y ≠ x
[PROOFSTEP]
simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
by_cases h : f y = x
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
constructor
[GOAL]
case pos.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ ↑f y ≠ y
[PROOFSTEP]
intro
[GOAL]
case pos.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
⊢ y ≠ x
[PROOFSTEP]
intro
[GOAL]
case pos.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : ↑f y = y
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case pos.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ↑f y = x
a✝ : y = x
⊢ False
[PROOFSTEP]
simp_all only [if_true, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hy : (if ↑f y = x then ↑f x else if y = x then x else ↑f y) ≠ y
h : ¬↑f y = x
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
split_ifs at hy  with hf heq
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f y = x
hf : ↑f y = x
hy : ↑f x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f y = x
hf : ¬↑f y = x
heq : y = x
hy : x ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f y = x
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
simp_all only [not_true]
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
h : ¬↑f x = x
heq : y = x
hy : x ≠ x
⊢ ↑f x ≠ x ∧ x ≠ x
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
exact ⟨h, hy⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hf : ¬↑f y = x
heq : ¬y = x
hy : ↑f y ≠ y
⊢ ↑f y ≠ y ∧ y ≠ x
[PROOFSTEP]
refine' ⟨hy, heq⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod l) x
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
h : f ∈ []
hl : List.Pairwise Disjoint []
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod []) x
[PROOFSTEP]
simp at h 
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
⊢ ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
intro x hx
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rw [List.pairwise_cons] at hl 
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f ∈ hd :: tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rw [List.mem_cons] at h 
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
h : f = hd ∨ f ∈ tl
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl✝ : List.Pairwise Disjoint l
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
x : α
hx : x ∈ support f
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint f a') ∧ List.Pairwise Disjoint tl
⊢ ↑f x = ↑(List.prod (f :: tl)) x
[PROOFSTEP]
rw [List.prod_cons, mul_apply, not_mem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
[GOAL]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x = ↑(List.prod (hd :: tl)) x
[PROOFSTEP]
rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← not_mem_support]
[GOAL]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ¬↑f x ∈ support hd
[PROOFSTEP]
refine' (hl.left _ h).symm.mem_imp _
[GOAL]
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : f ∈ l
hl✝ : List.Pairwise Disjoint l
hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ (x : α), x ∈ support f → ↑f x = ↑(List.prod tl) x
hl : (∀ (a' : Perm α), a' ∈ tl → Disjoint hd a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ support f
h : f ∈ tl
⊢ ↑f x ∈ support f
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : Disjoint f g
hf : support x ≤ support f
hg : support y ≤ support g
⊢ Disjoint x y
[PROOFSTEP]
rw [disjoint_iff_disjoint_support] at h ⊢
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
hf : support x ≤ support f
hg : support y ≤ support g
⊢ _root_.Disjoint (support x) (support y)
[PROOFSTEP]
exact h.mono hf hg
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ support f ≤ support (List.prod l)
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ support f
⊢ x ∈ support (List.prod l)
[PROOFSTEP]
rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ support (extendDomain g f) = map (asEmbedding f) (support g)
[PROOFSTEP]
ext b
[GOAL]
case a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ b ∈ support (extendDomain g f) ↔ b ∈ map (asEmbedding f) (support g)
[PROOFSTEP]
simp only [exists_prop, Function.Embedding.coeFn_mk, toEmbedding_apply, mem_map, Ne.def, Function.Embedding.trans_apply,
  mem_support]
[GOAL]
case a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ ¬↑(extendDomain g f) b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
by_cases pb : p b
[GOAL]
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(extendDomain g f) b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
rw [extendDomain_apply_subtype _ _ pb]
[GOAL]
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b → ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
rintro h
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
refine' ⟨f.symm ⟨b, pb⟩, _, by simp⟩
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ↑(asEmbedding f) (↑f.symm { val := b, property := pb }) = b
[PROOFSTEP]
simp
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ¬↑g (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
[PROOFSTEP]
contrapose! h
[GOAL]
case pos.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
h : ↑g (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
⊢ ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
[PROOFSTEP]
simp [h]
[GOAL]
case pos.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ (∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b) → ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
[PROOFSTEP]
rintro ⟨a, ha, hb⟩
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
ha : ¬↑g a = a
hb : ↑(asEmbedding f) a = b
⊢ ¬↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
[PROOFSTEP]
contrapose! ha
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : ↑(asEmbedding f) a = b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ↑g a = a
[PROOFSTEP]
obtain rfl : a = f.symm ⟨b, pb⟩ := by
  rw [eq_symm_apply]
  exact Subtype.coe_injective hb
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : ↑(asEmbedding f) a = b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ a = ↑f.symm { val := b, property := pb }
[PROOFSTEP]
rw [eq_symm_apply]
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
a : α
hb : ↑(asEmbedding f) a = b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
⊢ ↑f a = { val := b, property := pb }
[PROOFSTEP]
exact Subtype.coe_injective hb
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
hb : ↑(asEmbedding f) (↑f.symm { val := b, property := pb }) = b
⊢ ↑g (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
[PROOFSTEP]
rw [eq_symm_apply]
[GOAL]
case pos.mpr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
ha : ↑(↑f (↑g (↑f.symm { val := b, property := pb }))) = b
hb : ↑(asEmbedding f) (↑f.symm { val := b, property := pb }) = b
⊢ ↑f (↑g (↑f.symm { val := b, property := pb })) = { val := b, property := pb }
[PROOFSTEP]
exact Subtype.coe_injective ha
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬↑(extendDomain g f) b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
rw [extendDomain_apply_not_subtype _ _ pb]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ a, ¬↑g a = a ∧ ↑(asEmbedding f) a = b
[PROOFSTEP]
simp only [not_exists, false_iff_iff, not_and, eq_self_iff_true, not_true]
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ∀ (x : α), ¬↑g x = x → ¬↑(asEmbedding f) x = b
[PROOFSTEP]
rintro a _ rfl
[GOAL]
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
a : α
a✝ : ¬↑g a = a
pb : ¬p (↑(asEmbedding f) a)
⊢ False
[PROOFSTEP]
exact pb (Subtype.prop _)
[GOAL]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
f✝ g✝ : Perm α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ card (support (extendDomain g f)) = card (support g)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 0 ↔ f = 1
[PROOFSTEP]
rw [Finset.card_eq_zero, support_eq_empty_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ 1 < card (support f)
[PROOFSTEP]
simp_rw [one_lt_card_iff, mem_support, ← not_or]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(↑f a = a ∨ ↑f b = b ∨ a = b)
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
⊢ f = 1
[PROOFSTEP]
ext a
[GOAL]
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ∀ (a b : α), ↑f a = a ∨ ↑f b = b ∨ a = b
a : α
⊢ ↑f a = ↑1 a
[PROOFSTEP]
specialize h (f a) a
[GOAL]
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
a : α
h : ↑f (↑f a) = ↑f a ∨ ↑f a = a ∨ ↑f a = a
⊢ ↑f a = ↑1 a
[PROOFSTEP]
rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) ≠ 1
[PROOFSTEP]
by_cases h : f = 1
[GOAL]
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : f = 1
⊢ card (support f) ≠ 1
[PROOFSTEP]
exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one
[GOAL]
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : ¬f = 1
⊢ card (support f) ≠ 1
[PROOFSTEP]
exact ne_of_gt (one_lt_card_support_of_ne_one h)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) ≤ 1 ↔ f = 1
[PROOFSTEP]
rw [le_iff_lt_or_eq, Nat.lt_succ_iff, le_zero_iff, card_support_eq_zero, or_iff_not_imp_right,
  imp_iff_right f.card_support_ne_one]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
x : α
hx : ↑f x ≠ x
h : support f ⊆ support (swap x (↑f x) * f)
⊢ ¬↑(swap x (↑f x) * f) x ≠ x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ Multiset.Nodup (x ::ₘ y ::ₘ 0)
[PROOFSTEP]
simp [hxy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hxy : x ≠ y
⊢ support (swap x y) = { val := x ::ₘ y ::ₘ 0, nodup := (_ : Multiset.Nodup (x ::ₘ {y})) }
[PROOFSTEP]
simp [support_swap hxy, *, Finset.ext_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 2 ↔ IsSwap f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ card (support f) = 2 → IsSwap f
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
⊢ IsSwap f → card (support f) = 2
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : card (support f) = 2
⊢ IsSwap f
[PROOFSTEP]
obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
[GOAL]
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
[PROOFSTEP]
obtain ⟨y, rfl⟩ := card_eq_one.1 ht
[GOAL]
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
[PROOFSTEP]
rw [mem_singleton] at hmem 
[GOAL]
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
[PROOFSTEP]
refine' ⟨x, y, hmem, _⟩
[GOAL]
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
[PROOFSTEP]
ext a
[GOAL]
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
[PROOFSTEP]
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
[GOAL]
α : 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.195733 b
[PROOFSTEP]
rw [← mem_support, ← hins, mem_insert, mem_singleton]
[GOAL]
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
[PROOFSTEP]
by_cases ha : f a = a
[GOAL]
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
[PROOFSTEP]
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
[GOAL]
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
[PROOFSTEP]
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
[GOAL]
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
[PROOFSTEP]
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
[GOAL]
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
[PROOFSTEP]
obtain rfl | rfl := (key a).mp ha
[GOAL]
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
[PROOFSTEP]
rw [Or.resolve_left ha' ha, swap_apply_left]
[GOAL]
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
[PROOFSTEP]
rw [Or.resolve_right ha' ha, swap_apply_right]
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g f : Perm α
h : IsSwap f
⊢ card (support f) = 2
[PROOFSTEP]
obtain ⟨x, y, hxy, rfl⟩ := h
[GOAL]
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
[PROOFSTEP]
exact card_support_swap hxy
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ card (support (f * g)) = card (support f) + card (support g)
[PROOFSTEP]
rw [← Finset.card_disjoint_union]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ card (support (f * g)) = card (support f ∪ support g)
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ support (f * g) = support f ∪ support g
[PROOFSTEP]
ext
[GOAL]
case e_s.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
a✝ : α
⊢ a✝ ∈ support (f * g) ↔ a✝ ∈ support f ∪ support g
[PROOFSTEP]
simp [h.support_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : Disjoint f g
⊢ _root_.Disjoint (support f) (support g)
[PROOFSTEP]
simpa using h.disjoint_support
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ card (support (List.prod l)) = List.sum (List.map (card ∘ support) l)
[PROOFSTEP]
induction' l with a t ih
[GOAL]
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
h : List.Pairwise Disjoint []
⊢ card (support (List.prod [])) = List.sum (List.map (card ∘ support) [])
[PROOFSTEP]
exact card_support_eq_zero.mpr rfl
[GOAL]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → card (support (List.prod t)) = List.sum (List.map (card ∘ support) t)
h : List.Pairwise Disjoint (a :: t)
⊢ card (support (List.prod (a :: t))) = List.sum (List.map (card ∘ support) (a :: t))
[PROOFSTEP]
obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
[GOAL]
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → card (support (List.prod t)) = List.sum (List.map (card ∘ support) t)
h : List.Pairwise Disjoint (a :: t)
ha : ∀ (a' : Perm α), a' ∈ t → Disjoint a a'
ht : List.Pairwise Disjoint t
⊢ card (support (List.prod (a :: t))) = List.sum (List.map (card ∘ support) (a :: t))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
[GOAL]
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
h✝ : List.Pairwise Disjoint l
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → card (support (List.prod t)) = List.sum (List.map (card ∘ support) t)
h : List.Pairwise Disjoint (a :: t)
ha : ∀ (a' : Perm α), a' ∈ t → Disjoint a a'
ht : List.Pairwise Disjoint t
⊢ card (support (a * List.prod t)) = (card ∘ support) a + card (support (List.prod t))
[PROOFSTEP]
exact (disjoint_prod_right _ ha).card_support_mul
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
⊢ support (subtypePerm f h) = filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s
a✝ : { x // x ∈ s }
⊢ a✝ ∈ support (subtypePerm f h) ↔ a✝ ∈ filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (attach s)
[PROOFSTEP]
simp [Subtype.ext_iff]
