[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
a : Option α
⊢ a ∈ ↑insertNone univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Fintype α
⊢ ¬none ∈ map Embedding.some univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Trunc (P (ULift (Fin zero)))
[PROOFSTEP]
have : card PEmpty = card (ULift (Fin 0)) := by simp only [card_fin, card_pempty, card_ulift]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card PEmpty = card (ULift (Fin 0))
[PROOFSTEP]
simp only [card_fin, card_pempty, card_ulift]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty = card (ULift (Fin 0))
⊢ Trunc (P (ULift (Fin zero)))
[PROOFSTEP]
apply Trunc.bind (truncEquivOfCardEq this)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty = card (ULift (Fin 0))
⊢ PEmpty ≃ ULift (Fin 0) → Trunc (P (ULift (Fin zero)))
[PROOFSTEP]
intro e
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty = card (ULift (Fin 0))
e : PEmpty ≃ ULift (Fin 0)
⊢ Trunc (P (ULift (Fin zero)))
[PROOFSTEP]
apply Trunc.mk
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : card PEmpty = card (ULift (Fin 0))
e : PEmpty ≃ ULift (Fin 0)
⊢ P (ULift (Fin zero))
[PROOFSTEP]
refine' of_equiv e h_empty
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ Trunc (P (ULift (Fin (succ n))))
[PROOFSTEP]
have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by simp only [card_fin, card_option, card_ulift]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
[PROOFSTEP]
simp only [card_fin, card_option, card_ulift]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
this : card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
⊢ Trunc (P (ULift (Fin (succ n))))
[PROOFSTEP]
apply Trunc.bind (truncEquivOfCardEq this)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
this : card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
⊢ Option (ULift (Fin n)) ≃ ULift (Fin (succ n)) → Trunc (P (ULift (Fin (succ n))))
[PROOFSTEP]
intro e
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
this : card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
e : Option (ULift (Fin n)) ≃ ULift (Fin (succ n))
⊢ Trunc (P (ULift (Fin (succ n))))
[PROOFSTEP]
apply Trunc.map _ (ind n)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
this : card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
e : Option (ULift (Fin n)) ≃ ULift (Fin (succ n))
⊢ P (ULift (Fin n)) → P (ULift (Fin (succ n)))
[PROOFSTEP]
intro ih
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
this : card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
e : Option (ULift (Fin n)) ≃ ULift (Fin (succ n))
ih : P (ULift (Fin n))
⊢ P (ULift (Fin (succ n)))
[PROOFSTEP]
refine' of_equiv e (h_option ih)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Trunc (P α)
[PROOFSTEP]
suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n))
  by
  apply Trunc.bind (this (Fintype.card α))
  intro h
  apply Trunc.map _ (Fintype.truncEquivFin α)
  intro e
  exact of_equiv (Equiv.ulift.trans e.symm) h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift (Fin n)))
⊢ Trunc (P α)
[PROOFSTEP]
apply Trunc.bind (this (Fintype.card α))
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift (Fin n)))
⊢ P (ULift (Fin (card α))) → Trunc (P α)
[PROOFSTEP]
intro h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift (Fin n)))
h : P (ULift (Fin (card α)))
⊢ Trunc (P α)
[PROOFSTEP]
apply Trunc.map _ (Fintype.truncEquivFin α)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift (Fin n)))
h : P (ULift (Fin (card α)))
⊢ α ≃ Fin (card α) → P α
[PROOFSTEP]
intro e
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift (Fin n)))
h : P (ULift (Fin (card α)))
e : α ≃ Fin (card α)
⊢ P α
[PROOFSTEP]
exact of_equiv (Equiv.ulift.trans e.symm) h
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty
h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (n : ℕ) → Trunc (P (ULift (Fin n)))
[PROOFSTEP]
apply ind
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ P α
[PROOFSTEP]
obtain ⟨p⟩ :=
  let f_empty := fun i => by convert h_empty
  let h_option :
    ∀ {α : Type u} [Fintype α] [DecidableEq α], (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) :=
    by
    rintro α hα - Pα hα'
    convert h_option α (Pα _)
  @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _)) f_empty h_option α _
    (Classical.decEq α)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
i : Fintype PEmpty
⊢ P PEmpty
[PROOFSTEP]
convert h_empty
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
f_empty : ∀ (i : Fintype PEmpty), P PEmpty := fun i => ?m.7851 i
⊢ ∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
    (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)
[PROOFSTEP]
rintro α hα - Pα hα'
[GOAL]
α✝¹ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α✝ : Type u
h_fintype : Fintype α✝
f_empty : ∀ (i : Fintype PEmpty), P PEmpty := fun i => ?m.7851 i
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)
[PROOFSTEP]
convert h_option α (Pα _)
[GOAL]
case mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
x✝ : Trunc (∀ (h : Fintype α), P α)
p : ∀ (h : Fintype α), P α
⊢ P α
[PROOFSTEP]
exact
  p
    _
      -- ·
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
⊢ P α
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P α
[PROOFSTEP]
refine' Fintype.induction_empty_option _ _ _ α
[GOAL]
case intro.refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β
case intro.refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P PEmpty
case intro.refine'_3
α✝ : Type u_1
β : Type u_2
γ : Type u_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β
h_empty : P PEmpty
h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
[PROOFSTEP]
exacts [fun α β _ => of_equiv, h_empty, @h_option]


[GOAL]
n : ℕ
⊢ choose n 0 = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ choose zero 0 = 1
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ choose (succ n✝) 0 = 1
[PROOFSTEP]
rfl
[GOAL]
n k : ℕ
hk : n + 1 < k + 1
⊢ choose (n + 1) (k + 1) = 0
[PROOFSTEP]
have hnk : n < k := lt_of_succ_lt_succ hk
[GOAL]
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ choose (n + 1) (k + 1) = 0
[PROOFSTEP]
have hnk1 : n < k + 1 := lt_of_succ_lt hk
[GOAL]
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ choose (n + 1) (k + 1) = 0
[PROOFSTEP]
rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]
[GOAL]
n : ℕ
⊢ choose n n = 1
[PROOFSTEP]
induction n
[GOAL]
case zero
⊢ choose zero zero = 1
[PROOFSTEP]
simp [*, choose, choose_eq_zero_of_lt (lt_succ_self _)]
[GOAL]
case succ
n✝ : ℕ
n_ih✝ : choose n✝ n✝ = 1
⊢ choose (succ n✝) (succ n✝) = 1
[PROOFSTEP]
simp [*, choose, choose_eq_zero_of_lt (lt_succ_self _)]
[GOAL]
n : ℕ
⊢ choose n 1 = n
[PROOFSTEP]
induction n
[GOAL]
case zero
⊢ choose zero 1 = zero
[PROOFSTEP]
simp [*, choose, add_comm]
[GOAL]
case succ
n✝ : ℕ
n_ih✝ : choose n✝ 1 = n✝
⊢ choose (succ n✝) 1 = succ n✝
[PROOFSTEP]
simp [*, choose, add_comm]
[GOAL]
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
[PROOFSTEP]
rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, add_tsub_cancel_right, mul_comm]
[GOAL]
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ zero * (zero + 1) / 2 = zero * (zero - 1 + 2) / 2
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ succ n✝ * (succ n✝ + 1) / 2 = succ n✝ * (succ n✝ - 1 + 2) / 2
[PROOFSTEP]
rfl
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply zero_lt_succ
[GOAL]
n : ℕ
⊢ choose n 2 = n * (n - 1) / 2
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ choose zero 2 = zero * (zero - 1) / 2
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose (succ n) 2 = succ n * (succ n - 1) / 2
[PROOFSTEP]
rw [triangle_succ n, choose, ih]
[GOAL]
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose n 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
[PROOFSTEP]
simp [add_comm]
[GOAL]
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝
[PROOFSTEP]
rw [Nat.eq_zero_of_le_zero hk]
[GOAL]
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0
[PROOFSTEP]
decide
[GOAL]
n : ℕ
x✝ : 0 ≤ n + 1
⊢ 0 < choose (n + 1) 0
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ 0 < choose (n + 1) (k + 1)
[PROOFSTEP]
rw [choose_succ_succ]
[GOAL]
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ 0 < choose n k + choose n (succ k)
[PROOFSTEP]
exact add_pos_of_pos_of_nonneg (choose_pos (le_of_succ_le_succ hk)) (Nat.zero_le _)
[GOAL]
⊢ succ 0 * choose 0 0 = choose (succ 0) (succ 0) * succ 0
[PROOFSTEP]
decide
[GOAL]
k : ℕ
⊢ succ 0 * choose 0 (k + 1) = choose (succ 0) (succ (k + 1)) * succ (k + 1)
[PROOFSTEP]
simp [choose]
[GOAL]
n : ℕ
⊢ succ (n + 1) * choose (n + 1) 0 = choose (succ (n + 1)) (succ 0) * succ 0
[PROOFSTEP]
simp [choose, mul_succ, succ_eq_add_one, add_comm]
[GOAL]
n k : ℕ
⊢ succ (n + 1) * choose (n + 1) (k + 1) = choose (succ (n + 1)) (succ (k + 1)) * succ (k + 1)
[PROOFSTEP]
rw [choose_succ_succ (succ n) (succ k), add_mul, ← succ_mul_choose_eq n, mul_succ, ← succ_mul_choose_eq n,
  add_right_comm, ← mul_add, ← choose_succ_succ, ← succ_mul]
[GOAL]
x✝ : ℕ
hk : x✝ ≤ 0
⊢ choose 0 x✝ * x✝! * (0 - x✝)! = 0!
[PROOFSTEP]
simp [Nat.eq_zero_of_le_zero hk]
[GOAL]
n : ℕ
x✝ : 0 ≤ n + 1
⊢ choose (n + 1) 0 * 0! * (n + 1 - 0)! = (n + 1)!
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
cases' lt_or_eq_of_le hk with hk₁ hk₁
[GOAL]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! :=
  by
  rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
  simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose n k * (succ k)! * (n - k)! = (k + 1) * n !
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose n k * (succ k)! * (n - k)! = (k + 1) * (choose n k * k ! * (n - k)!)
[PROOFSTEP]
simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
⊢ (n - k)! = (n - k) * (n - succ k)!
[PROOFSTEP]
rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
[GOAL]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! :=
  by
  rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
  simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * (choose n (succ k) * (succ k)! * (n - succ k)!)
[PROOFSTEP]
simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
h₂ : choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
[GOAL]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
h₂ : choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul, tsub_mul, factorial_succ, ←
  add_tsub_assoc_of_le h₃, add_assoc, ← add_mul, add_tsub_cancel_left, add_comm]
[GOAL]
case inr
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k = n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
rw [hk₁]
[GOAL]
case inr
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k = n + 1
⊢ choose (n + 1) (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
[PROOFSTEP]
simp [hk₁, mul_comm, choose, tsub_self]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
⊢ (n - k)! * (k - s)! * s ! ≠ 0
[PROOFSTEP]
apply_rules [factorial_ne_zero, mul_ne_zero]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n k * choose k s * ((n - k)! * (k - s)! * s !) = choose n k * (choose k s * s ! * (k - s)!) * (n - k)!
[PROOFSTEP]
rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc _ s !, mul_assoc, mul_comm (n - k)!, mul_comm s !]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n k * (choose k s * s ! * (k - s)!) * (n - k)! = n !
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ n ! = choose n s * s ! * (choose (n - s) (k - s) * (k - s)! * (n - s - (k - s))!)
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial (tsub_le_tsub_right hkn _), choose_mul_factorial_mul_factorial (hsk.trans hkn)]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n s * s ! * (choose (n - s) (k - s) * (k - s)! * (n - s - (k - s))!) =
    choose n s * choose (n - s) (k - s) * ((n - k)! * (k - s)! * s !)
[PROOFSTEP]
rw [tsub_tsub_tsub_cancel_right hsk, mul_assoc, mul_left_comm s !, mul_assoc, mul_comm (k - s)!, mul_comm s !,
  mul_right_comm, ← mul_assoc]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ choose n k = n ! / (k ! * (n - k)!)
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ choose n k = choose n k * (k ! * (n - k)!) / (k ! * (n - k)!)
[PROOFSTEP]
exact (mul_div_left _ (mul_pos (factorial_pos _) (factorial_pos _))).symm
[GOAL]
i j : ℕ
⊢ choose (i + j) j = (i + j)! / (i ! * j !)
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), add_tsub_cancel_right, mul_comm]
[GOAL]
i j : ℕ
⊢ choose (i + j) j * i ! * j ! = (i + j)!
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), add_tsub_cancel_right, mul_right_comm]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ choose n k * (k ! * (n - k)!)
[PROOFSTEP]
exact dvd_mul_left _ _
[GOAL]
i j : ℕ
⊢ i ! * j ! ∣ (i + j)!
[PROOFSTEP]
suffices : i ! * (i + j - i)! ∣ (i + j)!
[GOAL]
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!
[PROOFSTEP]
rwa [add_tsub_cancel_left i j] at this
[GOAL]
case this
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
[PROOFSTEP]
exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ choose n (n - k) = choose n k
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _), tsub_tsub_cancel_of_le hk,
  mul_comm]
[GOAL]
n a b : ℕ
h : n = a + b
⊢ choose n a = choose n b
[PROOFSTEP]
suffices : choose n (n - b) = choose n b
[GOAL]
n a b : ℕ
h : n = a + b
this : choose n (n - b) = choose n b
⊢ choose n a = choose n b
[PROOFSTEP]
rw [h, add_tsub_cancel_right] at this
[GOAL]
n a b : ℕ
h : n = a + b
this : choose (a + b) a = choose (a + b) b
⊢ choose n a = choose n b
[PROOFSTEP]
rwa [h]
[GOAL]
case this
n a b : ℕ
h : n = a + b
⊢ choose n (n - b) = choose n b
[PROOFSTEP]
exact choose_symm (h ▸ le_add_left _ _)
[GOAL]
m : ℕ
⊢ choose (2 * m + 1) (m + 1) = choose (2 * m + 1) m
[PROOFSTEP]
apply choose_symm_of_eq_add
[GOAL]
case h
m : ℕ
⊢ 2 * m + 1 = m + 1 + m
[PROOFSTEP]
rw [add_comm m 1, add_assoc 1 m m, add_comm (2 * m) 1, two_mul m]
[GOAL]
n k : ℕ
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
[PROOFSTEP]
have e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
[GOAL]
case e
n k : ℕ
⊢ (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
[PROOFSTEP]
rw [← right_distrib, ← choose_succ_succ, succ_mul_choose_eq]
[GOAL]
n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
[PROOFSTEP]
rw [← tsub_eq_of_eq_add_rev e, mul_comm, ← mul_tsub, add_tsub_add_eq_tsub_right]
[GOAL]
n : ℕ
⊢ choose (n + 1 + 1) (n + 1) = n + 1 + 1
[PROOFSTEP]
rw [choose_succ_succ, choose_succ_self_right n, choose_self]
[GOAL]
n k : ℕ
⊢ choose n k * (n + 1) = choose (n + 1) k * (n + 1 - k)
[PROOFSTEP]
cases k with
| zero => simp
| succ k =>
  obtain hk | hk := le_or_lt (k + 1) (n + 1)
  ·
    rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
      add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
  · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
n k : ℕ
⊢ choose n k * (n + 1) = choose (n + 1) k * (n + 1 - k)
[PROOFSTEP]
cases k with
| zero => simp
| succ k =>
  obtain hk | hk := le_or_lt (k + 1) (n + 1)
  ·
    rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
      add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
  · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
case zero
n : ℕ
⊢ choose n zero * (n + 1) = choose (n + 1) zero * (n + 1 - zero)
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
n : ℕ
⊢ choose n zero * (n + 1) = choose (n + 1) zero * (n + 1 - zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n k : ℕ
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]

| succ k =>
  obtain hk | hk := le_or_lt (k + 1) (n + 1)
  ·
    rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
      add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
  · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
case succ
n k : ℕ
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]
obtain hk | hk := le_or_lt (k + 1) (n + 1)
[GOAL]
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]
rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
  add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
[GOAL]
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]
rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = k ! * choose (n + k) k
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = choose (n + k) k * k !
[PROOFSTEP]
apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
[GOAL]
n k : ℕ
⊢ ascFactorial n k * (n + k - k)! = choose (n + k) k * k ! * (n + k - k)!
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial, add_tsub_cancel_right, ← factorial_mul_ascFactorial, mul_comm]
[GOAL]
n k : ℕ
⊢ k ≤ n + k
[PROOFSTEP]
exact Nat.le_add_left k n
[GOAL]
n k : ℕ
⊢ choose (n + k) k = ascFactorial n k / k !
[PROOFSTEP]
apply mul_left_cancel₀ (factorial_ne_zero k)
[GOAL]
n k : ℕ
⊢ k ! * choose (n + k) k = k ! * (ascFactorial n k / k !)
[PROOFSTEP]
rw [← ascFactorial_eq_factorial_mul_choose]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = k ! * (ascFactorial n k / k !)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
[GOAL]
n k : ℕ
⊢ descFactorial n k = k ! * choose n k
[PROOFSTEP]
obtain h | h := Nat.lt_or_ge n k
[GOAL]
case inl
n k : ℕ
h : n < k
⊢ descFactorial n k = k ! * choose n k
[PROOFSTEP]
rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, mul_zero]
[GOAL]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = k ! * choose n k
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = choose n k * k !
[PROOFSTEP]
apply mul_right_cancel₀ (factorial_ne_zero (n - k))
[GOAL]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k * (n - k)! = choose n k * k ! * (n - k)!
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, mul_comm]
[GOAL]
n k : ℕ
⊢ choose n k = descFactorial n k / k !
[PROOFSTEP]
apply mul_left_cancel₀ (factorial_ne_zero k)
[GOAL]
n k : ℕ
⊢ k ! * choose n k = k ! * (descFactorial n k / k !)
[PROOFSTEP]
rw [← descFactorial_eq_factorial_mul_choose]
[GOAL]
n k : ℕ
⊢ descFactorial n k = k ! * (descFactorial n k / k !)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_descFactorial _ _).symm
[GOAL]
r n : ℕ
h : r < n / 2
⊢ choose n r ≤ choose n (r + 1)
[PROOFSTEP]
refine' le_of_mul_le_mul_right _ (lt_tsub_iff_left.mpr (lt_of_lt_of_le h (n.div_le_self 2)))
[GOAL]
r n : ℕ
h : r < n / 2
⊢ choose n r * (n - r) ≤ choose n (r + 1) * (n - r)
[PROOFSTEP]
rw [← choose_succ_right_eq]
[GOAL]
r n : ℕ
h : r < n / 2
⊢ choose n (r + 1) * (r + 1) ≤ choose n (r + 1) * (n - r)
[PROOFSTEP]
apply Nat.mul_le_mul_left
[GOAL]
case h
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r
[PROOFSTEP]
rw [← Nat.lt_iff_add_one_le, lt_tsub_iff_left, ← mul_two]
[GOAL]
case h
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
[PROOFSTEP]
exact lt_of_lt_of_le (mul_lt_mul_of_pos_right h zero_lt_two) (n.div_mul_le_self 2)
[GOAL]
r n : ℕ
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
cases' le_or_gt r n with b b
[GOAL]
case inl
r n : ℕ
b : r ≤ n
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
cases' le_or_lt r (n / 2) with a h
[GOAL]
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
apply choose_le_middle_of_le_half_left a
[GOAL]
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
rw [← choose_symm b]
[GOAL]
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n (n - r) ≤ choose n (n / 2)
[PROOFSTEP]
apply choose_le_middle_of_le_half_left
[GOAL]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2
[PROOFSTEP]
rw [div_lt_iff_lt_mul' zero_lt_two] at h
[GOAL]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n - r ≤ n / 2
[PROOFSTEP]
rw [le_div_iff_mul_le' zero_lt_two, tsub_mul, tsub_le_iff_tsub_le, mul_two, add_tsub_cancel_right]
[GOAL]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n ≤ r * 2
[PROOFSTEP]
exact le_of_lt h
[GOAL]
case inr
r n : ℕ
b : r > n
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
rw [choose_eq_zero_of_lt b]
[GOAL]
case inr
r n : ℕ
b : r > n
⊢ 0 ≤ choose n (n / 2)
[PROOFSTEP]
apply zero_le
[GOAL]
a c : ℕ
⊢ choose a c ≤ choose (succ a) c
[PROOFSTEP]
cases c
[GOAL]
case zero
a : ℕ
⊢ choose a zero ≤ choose (succ a) zero
[PROOFSTEP]
simp [Nat.choose_succ_succ]
[GOAL]
case succ
a n✝ : ℕ
⊢ choose a (succ n✝) ≤ choose (succ a) (succ n✝)
[PROOFSTEP]
simp [Nat.choose_succ_succ]
[GOAL]
a b c : ℕ
⊢ choose a c ≤ choose (a + b) c
[PROOFSTEP]
induction' b with b_n b_ih
[GOAL]
case zero
a c : ℕ
⊢ choose a c ≤ choose (a + zero) c
[PROOFSTEP]
simp
[GOAL]
case succ
a c b_n : ℕ
b_ih : choose a c ≤ choose (a + b_n) c
⊢ choose a c ≤ choose (a + succ b_n) c
[PROOFSTEP]
exact le_trans b_ih (choose_le_succ (a + b_n) c)
[GOAL]
n : ℕ
⊢ multichoose n 0 = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ multichoose zero 0 = 1
[PROOFSTEP]
simp [multichoose]
[GOAL]
case succ
n✝ : ℕ
⊢ multichoose (succ n✝) 0 = 1
[PROOFSTEP]
simp [multichoose]
[GOAL]
k : ℕ
⊢ multichoose 0 (k + 1) = 0
[PROOFSTEP]
simp [multichoose]
[GOAL]
n k : ℕ
⊢ multichoose (n + 1) (k + 1) = multichoose n (k + 1) + multichoose (n + 1) k
[PROOFSTEP]
simp [multichoose]
[GOAL]
k : ℕ
⊢ multichoose 1 k = 1
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
⊢ multichoose 1 zero = 1
[PROOFSTEP]
simp
[GOAL]
case succ
k : ℕ
IH : multichoose 1 k = 1
⊢ multichoose 1 (succ k) = 1
[PROOFSTEP]
simp [multichoose_succ_succ 0 k, IH]
[GOAL]
k : ℕ
⊢ multichoose 2 k = k + 1
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
⊢ multichoose 2 zero = zero + 1
[PROOFSTEP]
simp
[GOAL]
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (succ k) = succ k + 1
[PROOFSTEP]
rw [multichoose, IH]
[GOAL]
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = succ k + 1
[PROOFSTEP]
simp [add_comm, succ_eq_add_one]
[GOAL]
n : ℕ
⊢ multichoose n 1 = n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ multichoose zero 1 = zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
IH : multichoose n 1 = n
⊢ multichoose (succ n) 1 = succ n
[PROOFSTEP]
simp [multichoose_succ_succ n 0, IH]
[GOAL]
x✝ : ℕ
⊢ multichoose x✝ 0 = choose (x✝ + 0 - 1) 0
[PROOFSTEP]
simp
[GOAL]
k : ℕ
⊢ multichoose 0 (k + 1) = choose (0 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
have : n + (k + 1) < (n + 1) + (k + 1) := add_lt_add_right (Nat.lt_succ_self _) _
[GOAL]
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
have : (n + 1) + k < (n + 1) + (k + 1) := add_lt_add_left (Nat.lt_succ_self _) _
[GOAL]
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
[GOAL]
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) k + multichoose n (k + 1) = choose (n + k) k + choose (n + k) (succ k)
[PROOFSTEP]
simp [multichoose_eq n (k + 1), multichoose_eq (n + 1) k]
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n + 1, snd := k }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
{assumption
}
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n + 1, snd := k }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
assumption
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n, snd := k + 1 }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
{assumption
}
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n, snd := k + 1 }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
assumption


[GOAL]
α : Type u_1
n : ℕ
⊢ Even (card (Fin (bit0 n)))
[PROOFSTEP]
rw [Fintype.card_fin]
[GOAL]
α : Type u_1
n : ℕ
⊢ Even (bit0 n)
[PROOFSTEP]
exact even_bit0 _


[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀
[PROOFSTEP]
simpa using exists_max_image univ f univ_nonempty
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x
[PROOFSTEP]
simpa using exists_min_image univ f univ_nonempty


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ Fintype (Sym.Sym' α n)
[PROOFSTEP]
refine
  @Quotient.fintype _ _ _
    ?_
      -- Porting note: had to build the instance manually
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ DecidableRel fun x x_1 => x ≈ x_1
[PROOFSTEP]
intros x y
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
x y : Vector α n
⊢ Decidable ((fun x x_1 => x ≈ x_1) x y)
[PROOFSTEP]
apply List.decidablePerm


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
⊢ toFinset (s ×ˢ t) = toFinset s ×ˢ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ toFinset (s ×ˢ t) ↔ a✝ ∈ toFinset s ×ˢ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t s : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(offDiag s)
⊢ ∀ (a : α × α), a ∈ toFinset (offDiag s) ↔ a ∈ Finset.offDiag (toFinset s)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ univ ×ˢ univ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
[PROOFSTEP]
refine'
  ⟨fun H => _, fun H => H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
[PROOFSTEP]
rw [and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
[PROOFSTEP]
contrapose! H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
⊢ ¬Infinite (α × β)
[PROOFSTEP]
intro H'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
⊢ False
[PROOFSTEP]
rcases Infinite.nonempty (α × β) with ⟨a, b⟩
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
⊢ False
[PROOFSTEP]
haveI := fintypeOfNotInfinite (H.1 ⟨b⟩)
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this : Fintype α
⊢ False
[PROOFSTEP]
haveI := fintypeOfNotInfinite (H.2 ⟨a⟩)
[GOAL]
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this✝ : Fintype α
this : Fintype β
⊢ False
[PROOFSTEP]
exact H'.false
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
⊢ Infinite ((i : ι) → π i)
[PROOFSTEP]
choose m n hm using fun i => exists_pair_ne (π i)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
⊢ Infinite ((i : ι) → π i)
[PROOFSTEP]
refine' Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
h : (fun i => update m i (n i)) x = (fun i => update m i (n i)) y
hne : ¬x = y
⊢ False
[PROOFSTEP]
simp_rw [update_eq_iff, update_noteq hne] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type ?u.4746
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
hne : ¬x = y
h : n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update m y (n y) x_1
⊢ False
[PROOFSTEP]
exact (hm x h.1.symm).elim


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length (a :: l))!
[PROOFSTEP]
rw [length_cons, Nat.factorial_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length l + 1) * (length l)!
[PROOFSTEP]
simp only [permsOfList, length_append, length_permsOfList, length_bind, comp, length_map, map_const', sum_replicate,
  smul_eq_mul, succ_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ (length l)! + length l * (length l)! = length l * (length l)! + (length l)!
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ l
⊢ f ∈ permsOfList l
[PROOFSTEP]
induction l generalizing f with
| nil =>
  -- Porting note: applied `not_mem_nil` because it is no longer true definitionally.
  simp only [not_mem_nil] at h
  exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
| cons a l IH =>
  by_cases hfa : f a = a
  · refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
    by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx
    split_ifs at hx  with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
  refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ l
⊢ f ∈ permsOfList l
[PROOFSTEP]
induction l generalizing f with
| nil =>
  -- Porting note: applied `not_mem_nil` because it is no longer true definitionally.
  simp only [not_mem_nil] at h
  exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
| cons a l IH =>
  by_cases hfa : f a = a
  · refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
    by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx
    split_ifs at hx  with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
  refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
⊢ f ∈ permsOfList []
[PROOFSTEP]

| nil =>
  -- Porting note: applied `not_mem_nil` because it is no longer true definitionally.
  simp only [not_mem_nil] at h
  exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
⊢ f ∈ permsOfList []
[PROOFSTEP]
simp only [not_mem_nil] at h
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → False
⊢ f ∈ permsOfList []
[PROOFSTEP]
exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]

| cons a l IH =>
  by_cases hfa : f a = a
  · refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
    by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx
    split_ifs at hx  with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
  refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
by_cases hfa : f a = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ↑f a = a
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ↑f a = a
x : α
hx : ↑f x ≠ x
⊢ x ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
hx : ↑f x ≠ x
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ↑f x = x
⊢ False
[PROOFSTEP]
exact hx hfa
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
  by
  intro x hx
  have hxa : x ≠ a := by
    rintro rfl
    apply hx
    simp only [mul_apply, swap_apply_right]
  refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
  simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx
  split_ifs at hx  with h_1
  exacts [hxa (h.symm.trans h_1), hx h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
⊢ ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
⊢ x ∈ l
[PROOFSTEP]
have hxa : x ≠ a := by
  rintro rfl
  apply hx
  simp only [mul_apply, swap_apply_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
⊢ x ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬↑f x = x
hfa' : ↑f (↑f x) ≠ ↑f x
hx : ↑(Equiv.swap x (↑f x) * f) x ≠ x
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬↑f x = x
hfa' : ↑f (↑f x) ≠ ↑f x
hx : ↑(Equiv.swap x (↑f x) * f) x ≠ x
⊢ ↑(Equiv.swap x (↑f x) * f) x = x
[PROOFSTEP]
simp only [mul_apply, swap_apply_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
hxa : x ≠ a
⊢ x ∈ l
[PROOFSTEP]
refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
hxa : x ≠ a
h : ↑f x = x
⊢ False
[PROOFSTEP]
simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hxa : x ≠ a
h : ↑f x = x
hx : ¬(if ↑f x = a then ↑f a else if x = a then a else ↑f x) = x
⊢ False
[PROOFSTEP]
split_ifs at hx  with h_1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hxa : x ≠ a
h : ↑f x = x
h_1 : ↑f x = a
hx : ¬↑f a = x
⊢ False
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hxa : x ≠ a
h : ↑f x = x
h_1 : ¬↑f x = a
hx : ¬↑f x = x
⊢ False
[PROOFSTEP]
exacts [hxa (h.symm.trans h_1), hx h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
  simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this✝ : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
this : f ∈ permsOfList l ∨ ∃ b, b ∈ l ∧ ∃ g, g ∈ permsOfList l ∧ Equiv.swap a b * g = f
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l ∨ ∃ b, b ∈ l ∧ ∃ g, g ∈ permsOfList l ∧ Equiv.swap a b * g = f
[PROOFSTEP]
refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
_hfl : ¬f ∈ permsOfList l
⊢ ↑f a ∈ l
[PROOFSTEP]
exact mem_of_ne_of_mem hfa (h _ hfa')
[GOAL]
case neg.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
_hfl : ¬f ∈ permsOfList l
⊢ Equiv.swap a (↑f a) * (Equiv.swap a (↑f a) * f) = f
[PROOFSTEP]
rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ ↑f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
[PROOFSTEP]
have : f = 1 := by simpa [permsOfList] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f = 1
[PROOFSTEP]
simpa [permsOfList] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
this : f = 1
⊢ ↑f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
this : f = 1
⊢ ↑1 heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : x = a
⊢ x ∈ a :: l
[PROOFSTEP]
simp [hxa]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : x = y
⊢ x ∈ l
[PROOFSTEP]
rwa [hxy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ ↑g x ≠ x
[PROOFSTEP]
rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if ↑f x = a then y else if ↑f x = y then a else ↑f x) ≠ x
[PROOFSTEP]
split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if ↑f x = a then y else if ↑f x = y then a else ↑f x) ≠ x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝¹ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝ : ↑f x = a
⊢ y ≠ x
[PROOFSTEP]
exact Ne.symm hxy
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝² : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝¹ : ¬↑f x = a
h✝ : ↑f x = y
⊢ a ≠ x
[PROOFSTEP]
exact Ne.symm hxa
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝² : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝¹ : ¬↑f x = a
h✝ : ¬↑f x = y
⊢ ↑f x ≠ x
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝ : Nodup []
⊢ Nodup (permsOfList [])
[PROOFSTEP]
simp [permsOfList]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
have hl' : l.Nodup := hl.of_cons
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
  not_not.1 (mt (mem_of_mem_permsOfList hf _) (nodup_cons.1 hl).1)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
rw [permsOfList, List.nodup_append, List.nodup_bind, pairwise_iff_get]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l) ∧
    ((∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : Fin (length l)),
          i < j →
            List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
              (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))) ∧
      List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
[PROOFSTEP]
refine ⟨?_, ⟨⟨?_, ?_⟩, ?_⟩⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l)
[PROOFSTEP]
exact hln'
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))
[PROOFSTEP]
exact fun _ _ => hln'.map fun _ _ => mul_left_cancel
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (i j : Fin (length l)),
    i < j →
      List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
        (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))
[PROOFSTEP]
intros i j hij x hx₁ hx₂
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
⊢ False
[PROOFSTEP]
let ⟨f, hf⟩ := List.mem_map.1 hx₁
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
⊢ False
[PROOFSTEP]
let ⟨g, hg⟩ := List.mem_map.1 hx₂
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ False
[PROOFSTEP]
have hix : x a = List.get l i := by rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ ↑x a = List.get l i
[PROOFSTEP]
rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ False
[PROOFSTEP]
have hiy : x a = List.get l j := by rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ ↑x a = List.get l j
[PROOFSTEP]
rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
⊢ False
[PROOFSTEP]
have hieqj : i = j := nodup_iff_injective_get.1 hl' (hix.symm.trans hiy)
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
hieqj : i = j
⊢ False
[PROOFSTEP]
exact absurd hieqj (_root_.ne_of_lt hij)
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
[PROOFSTEP]
intros f hf₁ hf₂
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
⊢ False
[PROOFSTEP]
let ⟨x, hx, hx'⟩ := List.mem_bind.1 hf₂
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
⊢ False
[PROOFSTEP]
let ⟨g, hg⟩ := List.mem_map.1 hx'
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ False
[PROOFSTEP]
have hgxa : g⁻¹ x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ ↑f (↑g⁻¹ x) = ↑f a
[PROOFSTEP]
rw [hmeml hf₁, ← hg.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ ↑(Equiv.swap a x * g) (↑g⁻¹ x) = a
[PROOFSTEP]
simp
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : ↑g⁻¹ x = a
⊢ False
[PROOFSTEP]
have hxa : x ≠ a := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : ↑g⁻¹ x = a
hxa : x ≠ a
⊢ False
[PROOFSTEP]
exact (List.nodup_cons.1 hl).1 <| hgxa ▸ mem_of_mem_permsOfList hg.1 _ (by rwa [apply_inv_self, hgxa])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : ↑g⁻¹ x = a
hxa : x ≠ a
⊢ ↑g (↑g⁻¹ x) ≠ ↑g⁻¹ x
[PROOFSTEP]
rwa [apply_inv_self, hgxa]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
a b : List α
hab : a ≈ b
ha : Multiset.Nodup (Quotient.mk (isSetoid α) a)
hb : Multiset.Nodup (Quotient.mk (isSetoid α) b)
x✝ : HEq ha hb
⊢ ∀ (a_1 : Equiv.Perm α),
    a_1 ∈ { val := ↑(permsOfList a), nodup := (_ : Nodup (permsOfList a)) } ↔
      a_1 ∈ { val := ↑(permsOfList b), nodup := (_ : Nodup (permsOfList b)) }
[PROOFSTEP]
simp [mem_permsOfList_iff, hab.mem_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, ↑f x ≠ x → x ∈ s
[PROOFSTEP]
rintro ⟨⟨l⟩, hs⟩ f
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs } ↔
    ∀ {x : α}, ↑f x ≠ x → x ∈ { val := Quot.mk Setoid.r l, nodup := hs }
[PROOFSTEP]
exact mem_permsOfList_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ∀ (s : Finset α), card (permsOfFinset s) = (card s)!
[PROOFSTEP]
rintro ⟨⟨l⟩, hs⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ card (permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs }) = (card { val := Quot.mk Setoid.r l, nodup := hs })!
[PROOFSTEP]
exact length_permsOfList l
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Fintype α
⊢ ∀ (x : Equiv.Perm α), x ∈ permsOfFinset univ
[PROOFSTEP]
simp [mem_perms_of_finset_iff]