[GOAL]
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
[PROOFSTEP]
induction x using Fin.consInduction generalizing n with
| h0 =>
  cases n
  · simp
  · simp [eq_comm]
| h x₀ x ih =>
  simp_rw [Fin.sum_cons]
  rw [antidiagonalTuple]
    -- porting note: simp_rw doesn't use the equation lemma properly
  simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
    @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
    exists_eq_right]
[GOAL]
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
[PROOFSTEP]
induction x using Fin.consInduction generalizing n with
| h0 =>
  cases n
  · simp
  · simp [eq_comm]
| h x₀ x ih =>
  simp_rw [Fin.sum_cons]
  rw [antidiagonalTuple]
    -- porting note: simp_rw doesn't use the equation lemma properly
  simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
    @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
    exists_eq_right]
[GOAL]
case h0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i : Fin 0, Fin.elim0 i = n
[PROOFSTEP]

| h0 =>
  cases n
  · simp
  · simp [eq_comm]
[GOAL]
case h0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i : Fin 0, Fin.elim0 i = n
[PROOFSTEP]
cases n
[GOAL]
case h0.zero
k : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 Nat.zero ↔ ∑ i : Fin 0, Fin.elim0 i = Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (Nat.succ n✝) ↔ ∑ i : Fin 0, Fin.elim0 i = Nat.succ n✝
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i : Fin (n✝ + 1), Fin.cons x₀ x i = n
[PROOFSTEP]

| h x₀ x ih =>
  simp_rw [Fin.sum_cons]
  rw [antidiagonalTuple]
    -- porting note: simp_rw doesn't use the equation lemma properly
  simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
    @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
    exists_eq_right]
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i : Fin (n✝ + 1), Fin.cons x₀ x i = n
[PROOFSTEP]
simp_rw [Fin.sum_cons]
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ x₀ + ∑ i : Fin n✝, x i = n
[PROOFSTEP]
rw [antidiagonalTuple]
  -- porting note: simp_rw doesn't use the equation lemma properly
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ (Fin.cons x₀ x ∈
      List.bind (antidiagonal n) fun ni => map (fun x => Fin.cons ni.fst x) (antidiagonalTuple n✝ ni.snd)) ↔
    x₀ + ∑ i : Fin n✝, x i = n
[PROOFSTEP]
simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
  @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
  exists_eq_right]
[GOAL]
k n : ℕ
⊢ Nodup (antidiagonalTuple k n)
[PROOFSTEP]
induction' k with k ih generalizing n
[GOAL]
case zero
n✝ n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero n)
[PROOFSTEP]
cases n
[GOAL]
case zero.zero
n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case zero.succ
n n✝ : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero (Nat.succ n✝))
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ Nodup (antidiagonalTuple (Nat.succ k) n)
[PROOFSTEP]
simp_rw [antidiagonalTuple, List.nodup_bind]
[GOAL]
case succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ (∀ (x : ℕ × ℕ), x ∈ antidiagonal n → Nodup (map (fun x_1 => Fin.cons x.fst x_1) (antidiagonalTuple k x.snd))) ∧
    Pairwise
      (fun a b =>
        Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
          (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
      (antidiagonal n)
[PROOFSTEP]
constructor
[GOAL]
case succ.left
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ ∀ (x : ℕ × ℕ), x ∈ antidiagonal n → Nodup (map (fun x_1 => Fin.cons x.fst x_1) (antidiagonalTuple k x.snd))
[PROOFSTEP]
intro i _
[GOAL]
case succ.left
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
i : ℕ × ℕ
a✝ : i ∈ antidiagonal n
⊢ Nodup (map (fun x => Fin.cons i.fst x) (antidiagonalTuple k i.snd))
[PROOFSTEP]
exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)
[GOAL]
case succ.right
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
[PROOFSTEP]
induction' n with n n_ih
[GOAL]
case succ.right.zero
n k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal Nat.zero)
[PROOFSTEP]
exact List.pairwise_singleton _ _
[GOAL]
case succ.right.succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal (Nat.succ n))
[PROOFSTEP]
rw [List.Nat.antidiagonal_succ]
[GOAL]
case succ.right.succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n))
[PROOFSTEP]
refine' List.Pairwise.cons (fun a ha x hx₁ hx₂ => _) (n_ih.map _ fun a b h x hx₁ hx₂ => _)
[GOAL]
case succ.right.succ.refine'_1
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
ha : a ∈ map (Prod.map Nat.succ id) (antidiagonal n)
x : Fin (Nat.succ k) → ℕ
hx₁ : x ∈ map (fun x => Fin.cons (0, n + 1).fst x) (antidiagonalTuple k (0, n + 1).snd)
hx₂ : x ∈ map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd)
⊢ False
[PROOFSTEP]
rw [List.mem_map] at hx₁ hx₂ ha
[GOAL]
case succ.right.succ.refine'_1
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
ha : ∃ a_1, a_1 ∈ antidiagonal n ∧ Prod.map Nat.succ id a_1 = a
x : Fin (Nat.succ k) → ℕ
hx₁ : ∃ a, a ∈ antidiagonalTuple k (0, n + 1).snd ∧ Fin.cons (0, n + 1).fst a = x
hx₂ : ∃ a_1, a_1 ∈ antidiagonalTuple k a.snd ∧ Fin.cons a.fst a_1 = x
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
[GOAL]
case succ.right.succ.refine'_1.intro.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : Fin.cons (Prod.map Nat.succ id a).fst x₂ = Fin.cons (0, n + 1).fst x₁
⊢ False
[PROOFSTEP]
rw [Fin.cons_eq_cons] at h
[GOAL]
case succ.right.succ.refine'_1.intro.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : (Prod.map Nat.succ id a).fst = (0, n + 1).fst ∧ x₂ = x₁
⊢ False
[PROOFSTEP]
injection h.1
[GOAL]
case succ.right.succ.refine'_2
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x : Fin (Nat.succ k) → ℕ
hx₁ : x ∈ map (fun x => Fin.cons (Prod.map Nat.succ id a).fst x) (antidiagonalTuple k (Prod.map Nat.succ id a).snd)
hx₂ : x ∈ map (fun x => Fin.cons (Prod.map Nat.succ id b).fst x) (antidiagonalTuple k (Prod.map Nat.succ id b).snd)
⊢ False
[PROOFSTEP]
rw [List.mem_map] at hx₁ hx₂
[GOAL]
case succ.right.succ.refine'_2
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x : Fin (Nat.succ k) → ℕ
hx₁ : ∃ a_1, a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd ∧ Fin.cons (Prod.map Nat.succ id a).fst a_1 = x
hx₂ : ∃ a, a ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd ∧ Fin.cons (Prod.map Nat.succ id b).fst a = x
⊢ False
[PROOFSTEP]
obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : Fin.cons (Prod.map Nat.succ id b).fst x₂ = Fin.cons (Prod.map Nat.succ id a).fst x₁
⊢ False
[PROOFSTEP]
dsimp at h₁₂
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : Fin.cons (Nat.succ b.fst) x₂ = Fin.cons (Nat.succ a.fst) x₁
⊢ False
[PROOFSTEP]
rw [Fin.cons_eq_cons, Nat.succ_inj'] at h₁₂
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : b.fst = a.fst ∧ x₂ = x₁
⊢ False
[PROOFSTEP]
obtain ⟨h₁₂, rfl⟩ := h₁₂
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : b.fst = a.fst
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
⊢ False
[PROOFSTEP]
rw [h₁₂] at h
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k b.snd))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : b.fst = a.fst
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
⊢ False
[PROOFSTEP]
exact h (List.mem_map_of_mem _ hx₁) (List.mem_map_of_mem _ hx₂)
[GOAL]
k : ℕ
⊢ antidiagonalTuple (k + 1) 0 = [0]
[PROOFSTEP]
rw [antidiagonalTuple, antidiagonal_zero, List.bind_singleton, antidiagonalTuple_zero_right k, List.map_singleton]
[GOAL]
k : ℕ
⊢ [Fin.cons (0, 0).fst 0] = [0]
[PROOFSTEP]
exact congr_arg (fun x => [x]) Matrix.cons_zero_zero
[GOAL]
n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]
[PROOFSTEP]
simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton, tsub_self,
  List.append_bind, List.bind_singleton, List.map_bind]
[GOAL]
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]
[PROOFSTEP]
conv_rhs => rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
| [![n]]
[PROOFSTEP]
rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
| [![n]]
[PROOFSTEP]
rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
| [![n]]
[PROOFSTEP]
rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) = []
[PROOFSTEP]
simp_rw [List.bind_eq_nil, List.mem_range, List.map_eq_nil]
[GOAL]
case e_a
n : ℕ
⊢ ∀ (x : ℕ), x < n → antidiagonalTuple 0 (n - x) = []
[PROOFSTEP]
intro x hx
[GOAL]
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []
[PROOFSTEP]
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx
[GOAL]
case e_a.intro
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]
[GOAL]
n : ℕ
⊢ antidiagonalTuple 2 n = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
[PROOFSTEP]
rw [antidiagonalTuple]
[GOAL]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => map (fun x => Fin.cons ni.fst x) (antidiagonalTuple 1 ni.snd)) =
    map (fun i => ![i.fst, i.snd]) (antidiagonal n)
[PROOFSTEP]
simp_rw [antidiagonalTuple_one, List.map_singleton]
[GOAL]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
[PROOFSTEP]
rw [List.map_eq_bind]
[GOAL]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) =
    List.bind (antidiagonal n) fun x => [![x.fst, x.snd]]
[PROOFSTEP]
rfl
[GOAL]
k n : ℕ
⊢ Pairwise (Pi.Lex (fun x x_1 => x < x_1) fun x x x_1 => x < x_1) (antidiagonalTuple (k + 1) n)
[PROOFSTEP]
simp_rw [antidiagonalTuple, List.pairwise_bind, List.pairwise_map, List.mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂]
[GOAL]
k n : ℕ
⊢ (∀ (a : ℕ × ℕ),
      a ∈ antidiagonal n →
        Pairwise
          (fun a_2 b => Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a.fst a_2) (Fin.cons a.fst b))
          (antidiagonalTuple (Nat.add k 0) a.snd)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
                Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a₁.fst a) (Fin.cons a₂.fst a_2))
      (antidiagonal n)
[PROOFSTEP]
simp only [mem_antidiagonal, Prod.forall, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a_2 b => Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a a_2) (Fin.cons a b))
          (antidiagonalTuple (Nat.add k 0) b)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
                Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a₁.fst a) (Fin.cons a₂.fst a_2))
      (antidiagonal n)
[PROOFSTEP]
simp only [Fin.pi_lex_lt_cons_cons, eq_self_iff_true, true_and_iff, lt_self_iff_false, false_or_iff]
[GOAL]
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a b => Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a b)
          (antidiagonalTuple (Nat.add k 0) b)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
                a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
      (antidiagonal n)
[PROOFSTEP]
refine' ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, _⟩
[GOAL]
k n : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
[PROOFSTEP]
induction' n with n n_ih
[GOAL]
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal Nat.zero)
[PROOFSTEP]
rw [antidiagonal_zero]
[GOAL]
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    [(0, 0)]
[PROOFSTEP]
exact List.pairwise_singleton _ _
[GOAL]
case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal (Nat.succ n))
[PROOFSTEP]
rw [antidiagonal_succ, List.pairwise_cons, List.pairwise_map]
[GOAL]
case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ (∀ (a' : ℕ × ℕ),
      a' ∈ map (Prod.map Nat.succ id) (antidiagonal n) →
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a'.snd →
                (0, n + 1).fst < a'.fst ∨
                  (0, n + 1).fst = a'.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2) ∧
    Pairwise
      (fun a b =>
        ∀ (a_1 : Fin (Nat.add k 0) → ℕ),
          a_1 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id a).snd →
            ∀ (a_3 : Fin (Nat.add k 0) → ℕ),
              a_3 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id b).snd →
                (Prod.map Nat.succ id a).fst < (Prod.map Nat.succ id b).fst ∨
                  (Prod.map Nat.succ id a).fst = (Prod.map Nat.succ id b).fst ∧
                    Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
      (antidiagonal n)
[PROOFSTEP]
refine' ⟨fun p hp x hx y hy => _, _⟩
[GOAL]
case succ.refine'_1
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
p : ℕ × ℕ
hp : p ∈ map (Prod.map Nat.succ id) (antidiagonal n)
x : Fin (Nat.add k 0) → ℕ
hx : x ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd
y : Fin (Nat.add k 0) → ℕ
hy : y ∈ antidiagonalTuple (Nat.add k 0) p.snd
⊢ (0, n + 1).fst < p.fst ∨ (0, n + 1).fst = p.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
rw [List.mem_map, Prod.exists] at hp
[GOAL]
case succ.refine'_1
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
p : ℕ × ℕ
hp : ∃ a b, (a, b) ∈ antidiagonal n ∧ Prod.map Nat.succ id (a, b) = p
x : Fin (Nat.add k 0) → ℕ
hx : x ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd
y : Fin (Nat.add k 0) → ℕ
hy : y ∈ antidiagonalTuple (Nat.add k 0) p.snd
⊢ (0, n + 1).fst < p.fst ∨ (0, n + 1).fst = p.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
obtain ⟨a, b, _, rfl : (Nat.succ a, b) = p⟩ := hp
[GOAL]
case succ.refine'_1.intro.intro.intro
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
x : Fin (Nat.add k 0) → ℕ
hx : x ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd
y : Fin (Nat.add k 0) → ℕ
a b : ℕ
left✝ : (a, b) ∈ antidiagonal n
hy : y ∈ antidiagonalTuple (Nat.add k 0) (Nat.succ a, b).snd
⊢ (0, n + 1).fst < (Nat.succ a, b).fst ∨
    (0, n + 1).fst = (Nat.succ a, b).fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
exact Or.inl (Nat.zero_lt_succ _)
[GOAL]
case succ.refine'_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ (a_1 : Fin (Nat.add k 0) → ℕ),
        a_1 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id a).snd →
          ∀ (a_3 : Fin (Nat.add k 0) → ℕ),
            a_3 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id b).snd →
              (Prod.map Nat.succ id a).fst < (Prod.map Nat.succ id b).fst ∨
                (Prod.map Nat.succ id a).fst = (Prod.map Nat.succ id b).fst ∧
                  Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
    (antidiagonal n)
[PROOFSTEP]
dsimp
[GOAL]
case succ.refine'_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ (a_1 : Fin k → ℕ),
        a_1 ∈ antidiagonalTuple k a.snd →
          ∀ (a_3 : Fin k → ℕ),
            a_3 ∈ antidiagonalTuple k b.snd →
              Nat.succ a.fst < Nat.succ b.fst ∨
                Nat.succ a.fst = Nat.succ b.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
    (antidiagonal n)
[PROOFSTEP]
simp_rw [Nat.succ_inj', Nat.succ_lt_succ_iff]
[GOAL]
case succ.refine'_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ (a_1 : Fin k → ℕ),
        a_1 ∈ antidiagonalTuple k a.snd →
          ∀ (a_3 : Fin k → ℕ),
            a_3 ∈ antidiagonalTuple k b.snd →
              a.fst < b.fst ∨ a.fst = b.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
    (antidiagonal n)
[PROOFSTEP]
exact n_ih


[GOAL]
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
⊢ p < q ↔ p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p
[PROOFSTEP]
rw [lt_iff_le_not_le, not_le_iff_exists]


[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)
[PROOFSTEP]
simp_rw [seq, seq_eq]
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
[PROOFSTEP]
refine' i.cases _ fun i => _
[GOAL]
case refine'_1
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) (Fin.succ i) =
    f (Fin.succ i) (v (Fin.succ i))
[PROOFSTEP]
rw [Matrix.cons_val_succ]
[GOAL]
case refine'_2
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f (Fin.succ i) (v (Fin.succ i))
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x
[PROOFSTEP]
simp only [Forall, Fin.forall_fin_zero_pi]
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim
[PROOFSTEP]
rfl
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
P : (Fin (Nat.succ n) → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin (Nat.succ n) → α), P x
[PROOFSTEP]
simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x
[PROOFSTEP]
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
[GOAL]
m n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0' ↔ P finZeroElim
[PROOFSTEP]
rfl
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
P : (Fin (Nat.succ n) → α) → Prop
⊢ Exists P ↔ ∃ x, P x
[PROOFSTEP]
simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]
[GOAL]
m n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ sum a = ∑ i : Fin (n + 2), a i
[PROOFSTEP]
rw [Fin.sum_univ_castSucc, sum, sum_eq]


[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card (graph f) = n
[PROOFSTEP]
rw [graph, Finset.card_image_of_injective]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card Finset.univ = n
[PROOFSTEP]
exact Finset.card_fin _
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Function.Injective fun i => (f i, i)
[PROOFSTEP]
intro _
  _
    -- Porting note: was `simp`
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (fun i => (f i, i)) a₁✝ = (fun i => (f i, i)) a₂✝ → a₁✝ = a₂✝
[PROOFSTEP]
dsimp only
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝) = (f a₂✝, a₂✝) → a₁✝ = a₂✝
[PROOFSTEP]
rw [Prod.ext_iff]
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝).fst = (f a₂✝, a₂✝).fst ∧ (f a₁✝, a₁✝).snd = (f a₂✝, a₂✝).snd → a₁✝ = a₂✝
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (f i, i) ∈ graph f
[PROOFSTEP]
simp [graph]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (fun p => (↑p).snd)
      ((fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) }) i) =
    i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i : Fin n
h : (x, i) ∈ graph f
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i), property := h }) =
    { val := (x, i), property := h }
[PROOFSTEP]
simp only [graph, Finset.mem_image, Finset.mem_univ, true_and] at h
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i : Fin n
h✝ : (x, i) ∈ graph f
h : ∃ a, (f a, a) = (x, i)
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i), property := h✝ }) =
    { val := (x, i), property := h✝ }
[PROOFSTEP]
obtain ⟨i', hi'⟩ := h
[GOAL]
case intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i : Fin n
h : (x, i) ∈ graph f
i' : Fin n
hi' : (f i', i') = (x, i)
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i), property := h }) =
    { val := (x, i), property := h }
[PROOFSTEP]
obtain ⟨-, rfl⟩ := Prod.mk.inj_iff.mp hi'
[GOAL]
case intro.intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i' : Fin n
h : (x, i') ∈ graph f
hi' : (f i', i') = (x, i')
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i'), property := h }) =
    { val := (x, i'), property := h }
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card (graph f) = n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ graph.proj ∘ (↑(graphEquiv₁ f) ∘ ↑(graphEquiv₁ f).symm) ∘ ↑(graphEquiv₂ f).toEquiv = graph.proj ∘ ↑(graphEquiv₂ f)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone graph.proj
[PROOFSTEP]
rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (_ | h)
[GOAL]
case mk.mk.mk.mk.left
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
y : α
j : Fin n
hy : (y, j) ∈ graph f
h✝ : x < y
⊢ graph.proj { val := (x, i), property := hx } ≤ graph.proj { val := (y, j), property := hy }
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case mk.mk.mk.mk.right
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
j : Fin n
hy : (x, j) ∈ graph f
h✝ : i ≤ j
⊢ graph.proj { val := (x, i), property := hx } ≤ graph.proj { val := (x, j), property := hy }
[PROOFSTEP]
simp [graph.proj]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (f ∘ ↑(sort f))
[PROOFSTEP]
rw [self_comp_sort]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (graph.proj ∘ ↑(graphEquiv₂ f))
[PROOFSTEP]
exact (monotone_proj f).comp (graphEquiv₂ f).monotone
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ StrictMono ↑(σ.trans (graphEquiv₁ f))
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f → StrictMono ↑(σ.trans (graphEquiv₁ f))
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f)) → σ = sort f
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f))
[PROOFSTEP]
rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]
[GOAL]
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑((graphEquiv₂ f).trans (Equiv.refl { x // x ∈ graph f }))
[PROOFSTEP]
exact (graphEquiv₂ f).strictMono
[GOAL]
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
⊢ σ = sort f
[PROOFSTEP]
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
[GOAL]
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
this :
  graphEquiv₂ f =
    StrictMono.orderIsoOfSurjective (↑(σ.trans (graphEquiv₁ f))) h (_ : Function.Surjective ↑(σ.trans (graphEquiv₁ f)))
⊢ σ = sort f
[PROOFSTEP]
ext1 x
[GOAL]
case mpr.H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
this :
  graphEquiv₂ f =
    StrictMono.orderIsoOfSurjective (↑(σ.trans (graphEquiv₁ f))) h (_ : Function.Surjective ↑(σ.trans (graphEquiv₁ f)))
x : Fin n
⊢ ↑σ x = ↑(sort f) x
[PROOFSTEP]
exact (graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (FunLike.congr_fun this x).symm
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
[PROOFSTEP]
rw [eq_sort_iff']
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f)) ↔ Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
[PROOFSTEP]
refine' ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => _⟩, fun h i j hij => _⟩
[GOAL]
case refine'_1
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
i j : Fin n
hij : i < j
hfij : f (↑σ i) = f (↑σ j)
⊢ ↑σ i < ↑σ j
[PROOFSTEP]
exact (((Prod.Lex.lt_iff _ _).1 <| h hij).resolve_left hfij.not_lt).2
[GOAL]
case refine'_2
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
[PROOFSTEP]
obtain he | hl := (h.1 hij.le).eq_or_lt
[GOAL]
case refine'_2.inl
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
he : (f ∘ ↑σ) i = (f ∘ ↑σ) j
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
[PROOFSTEP]
apply (Prod.Lex.lt_iff _ _).2
[GOAL]
case refine'_2.inr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
hl : (f ∘ ↑σ) i < (f ∘ ↑σ) j
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
[PROOFSTEP]
apply (Prod.Lex.lt_iff _ _).2
[GOAL]
case refine'_2.inl
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
he : (f ∘ ↑σ) i = (f ∘ ↑σ) j
⊢ (f (↑σ i), ↑σ i).fst < (f (↑σ j), ↑σ j).fst ∨
    (f (↑σ i), ↑σ i).fst = (f (↑σ j), ↑σ j).fst ∧ (f (↑σ i), ↑σ i).snd < (f (↑σ j), ↑σ j).snd
case refine'_2.inr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
hl : (f ∘ ↑σ) i < (f ∘ ↑σ) j
⊢ (f (↑σ i), ↑σ i).fst < (f (↑σ j), ↑σ j).fst ∨
    (f (↑σ i), ↑σ i).fst = (f (↑σ j), ↑σ j).fst ∧ (f (↑σ i), ↑σ i).snd < (f (↑σ j), ↑σ j).snd
[PROOFSTEP]
exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ sort f = Equiv.refl (Fin n) ↔ Monotone f
[PROOFSTEP]
rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp.right_id]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f
[PROOFSTEP]
simp only [id.def, and_iff_left_iff_imp]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j
[PROOFSTEP]
exact fun _ _ _ hij _ => hij
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ (f ∘ ↑σ) ∘ ↑(sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
[PROOFSTEP]
rw [Function.comp.assoc, ← Equiv.Perm.coe_mul]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ f ∘ ↑(σ * sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
[PROOFSTEP]
exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : f ∘ ↑σ ≠ f ∘ ↑(sort f)
⊢ ∃ i j, i < j ∧ (f ∘ ↑σ) j < (f ∘ ↑σ) i
[PROOFSTEP]
contrapose! h
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ↑σ) i ≤ (f ∘ ↑σ) j
⊢ f ∘ ↑σ = f ∘ ↑(sort f)
[PROOFSTEP]
exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)