awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x : List α
h : L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L
⊢ x ∈ L.toDFA.accepts ↔ x ∈ L

Tactic:
rw [DFA.mem_accepts]

Premises used: DFA.mem_accepts
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x : List α
this : (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L

Tactic:
simp [this]
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x : List α
h : (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L

Tactic:
suffices L.toDFA.eval x = L.leftQuotient x by simp [this]
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
⊢ (↑(L.toDFA.eval []) : Language α) = L.leftQuotient []

Tactic:
simp
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x : List α
a : α
ih : (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x
⊢ (↑(L.toDFA.eval (x ++ [a])) : Language α) = L.leftQuotient (x ++ [a])

Tactic:
simp [ih, leftQuotient_append]

Premises used: Language.leftQuotient_append
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x : List α
h : (↑(L.toDFA.eval []) : Language α) = L.leftQuotient []
h₁ :
  ∀ (x : List α) (a : α) (ih : (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x),
    (↑(L.toDFA.eval (x ++ [a])) : Language α) = L.leftQuotient (x ++ [a])
⊢ (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x

Tactic:
induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih, leftQuotient_append]

Premises used: Language.leftQuotient_append
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
h : (Set.range L.leftQuotient).Finite
⊢ L.toDFA.accepts = L

Tactic:
simp
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
⊢ L.IsRegular ↔ (Set.range L.leftQuotient).Finite

Tactic:
⟨IsRegular.finite_range_leftQuotient, .of_finite_range_leftQuotient⟩

Premises used: Language.IsRegular.of_finite_range_leftQuotient, Iff.intro, Language.IsRegular.finite_range_leftQuotient
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
xy : ℕ × ℕ
rw : xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ : Finset (ℕ × ℕ) }.val ↔ xy.1 + xy.2 = n
rw₁ rw₂ : xy.1 + xy.2 = n ↔ xy.1 + xy.2 = n
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ : Finset (ℕ × ℕ) } ↔ xy.1 + xy.2 = n

Tactic:
rw [mem_def, Multiset.Nat.mem_antidiagonal]

Premises used: Multiset.Nat.mem_antidiagonal, Finset.mem_def
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ n = map { toFun := fun (i : ℕ) ↦ (i, n - i), inj' := ⋯ } (range (n + 1))

Tactic:
rfl

Premises used: Multiset.map, Finset.map, Multiset.Nat.antidiagonal, rfl, List.Nat.antidiagonal
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
rw :
  Eq (α := Finset (ℕ × ℕ))
    (map
      (Embedding.trans { toFun := fun (i : ℕ) ↦ (i, n - i), inj' := ⋯ }
        { toFun := Prod.swap, inj' := ⋯ : ℕ × ℕ ↪ ℕ × ℕ })
      (range (n + 1)))
    (map { toFun := fun (i : ℕ) ↦ (n - i, i), inj' := ⋯ } (range (n + 1)))
⊢ @antidiagonal _ Nat.instAddMonoid _ n = map { toFun := fun (i : ℕ) ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
rw [← map_swap_antidiagonal, antidiagonal_eq_map, map_map]

Premises used: Finset.Nat.antidiagonal_eq_map, Finset.map_swap_antidiagonal, Finset.map_map
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := Finset (ℕ × ℕ))
    (map
      (Embedding.trans { toFun := fun (i : ℕ) ↦ (i, n - i), inj' := ⋯ }
        { toFun := Prod.swap, inj' := ⋯ : ℕ × ℕ ↪ ℕ × ℕ })
      (range (n + 1)))
    (map { toFun := fun (i : ℕ) ↦ (n - i, i), inj' := ⋯ } (range (n + 1)))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ n = image (fun (i : ℕ) ↦ (i, n - i)) (range (n + 1))

Tactic:
simp only [antidiagonal_eq_map, map_eq_image, Function.Embedding.coeFn_mk]

Premises used: Finset.Nat.antidiagonal_eq_map, Finset.map_eq_image, Function.Embedding.coeFn_mk
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ n = image (fun (i : ℕ) ↦ (n - i, i)) (range (n + 1))

Tactic:
simp only [antidiagonal_eq_map', map_eq_image, Function.Embedding.coeFn_mk]

Premises used: Finset.map_eq_image, Function.Embedding.coeFn_mk, Finset.Nat.antidiagonal_eq_map'
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ #(@antidiagonal _ Nat.instAddMonoid _ n) = n + 1

Tactic:
simp [antidiagonal]

Premises used: Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 0) {(0, 0)}

Tactic:
rfl

Premises used: List.map, Multiset.cons, Multiset.Nat.antidiagonal, Multiset.ofList, rfl, List.Nat.antidiagonal
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (0, n + 1) ∉
    map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
      (@antidiagonal _ Nat.instAddMonoid _ n)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
a :
  (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
    (cons (0, n + 1)
        (map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯).val
⊢ @antidiagonal _ Nat.instAddMonoid _ (n + 1) =
    cons (0, n + 1)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ n))
      ⋯

Tactic:
apply eq_of_veq

Premises used: Finset.eq_of_veq
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map
        (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)) : (a : ℕ × ℕ) → ℕ × ℕ)
        (@antidiagonal _ Nat.instAddMonoid _ n).val

Tactic:
apply Multiset.Nat.antidiagonal_succ

Premises used: Multiset.Nat.antidiagonal_succ
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (n + 1, 0) ∉
    map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ n)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
a :
  (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
    (cons (n + 1, 0)
        (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯).val
⊢ @antidiagonal _ Nat.instAddMonoid _ (n + 1) =
    cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      ⋯

Tactic:
apply eq_of_veq

Premises used: Finset.eq_of_veq
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map
        (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }) : (a : ℕ × ℕ) → ℕ × ℕ)
        (@antidiagonal _ Nat.instAddMonoid _ n).val

Tactic:
Multiset.Nat.antidiagonal_succ'

Premises used: Multiset.Nat.antidiagonal, Prod.map, Multiset.Nat.antidiagonal_succ', Multiset.ofList
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map
        (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }) : (a : ℕ × ℕ) → ℕ × ℕ)
        (@antidiagonal _ Nat.instAddMonoid _ n).val

Tactic:
exact Multiset.Nat.antidiagonal_succ'

Premises used: Multiset.Nat.antidiagonal_succ'
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (n + 2, 0) ∉
    map
      ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
        { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ n)

Tactic:
simp
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ (0, n + 2) ∉
    cons (n + 2, 0)
      (map
        ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
          { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      ⋯

Tactic:
simp
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
simp_rw :
  cons (0, n + 1 + 1)
      (cons
        (({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ) : (a : ℕ × ℕ) → ℕ × ℕ)
          (n + 1, 0))
        (map
          (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }).trans
            ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)))
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
            { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯)
      ⋯
⊢ @antidiagonal _ Nat.instAddMonoid _ (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
            { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯)
      ⋯

Tactic:
simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]

Premises used: Finset.Nat.antidiagonal_succ, Finset.map_cons, HAdd.hAdd, OfNat.ofNat, Finset.map_map, Finset.Nat.antidiagonal_succ'
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons
        (({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ) : (a : ℕ × ℕ) → ℕ × ℕ)
          (n + 1, 0))
        (map
          (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }).trans
            ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)))
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
            { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯)
      ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ kl.1 < n + 1

Tactic:
Nat.lt_succ_of_le <| antidiagonal.fst_le hlk

Premises used: Nat.lt_succ_of_le, Finset.antidiagonal.fst_le
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n : ℕ
kl : ℕ × ℕ
hlk : kl ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ kl.2 < n + 1

Tactic:
Nat.lt_succ_of_le <| antidiagonal.snd_le hlk

Premises used: Nat.lt_succ_of_le, Finset.antidiagonal.snd_le
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
h₁ :
  ∀ (i j : ℕ),
    (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} ↔
      (i, j) ∈
        map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (@antidiagonal _ Nat.instAddMonoid _ k)
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} =
    map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
      (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
ext ⟨i, j⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i
⊢ (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
simpa
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
h₁ : i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i
⊢ (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i

Tactic:
⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩

Premises used: HSub.hSub, tsub_add_cancel_of_le, And.right, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
h₁ : ∀ (hi : i + j = n ∧ j ≤ k), k - j + (n - k) = i
h₂ : (∃ (a : ℕ), a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
⊢ i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i

Tactic:
refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
h₁ : n - k + (k - j) = i
h₂ : n + (k - j) - k = i
h₃ : i + j + (k - j) - k = i
h₄ : i + (j + (k - j)) - k = i
h₅ : i + k - k = i
h₆ h₇ : i = i
⊢ k - j + (n - k) = i

Tactic:
rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]

Premises used: add_assoc, Nat.add_sub_of_le, add_comm, tsub_add_eq_add_tsub, And.right, And.left, add_tsub_cancel_right
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k

Tactic:
⟨?_, hl ▸ Nat.le_add_left j l⟩

Premises used: Nat.le_add_left, Eq.rec, And.intro
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
h₁ : l + (n - k) + j = n
⊢ l + (n - k) + j = n ∧ j ≤ k

Tactic:
refine ⟨?_, hl ▸ Nat.le_add_left j l⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
h₁ : n - k + k = n
⊢ l + (n - k) + j = n

Tactic:
rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n

Tactic:
Nat.sub_add_cancel h

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n

Tactic:
exact Nat.sub_add_cancel h

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
⊢ Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))

Tactic:
have aux₁ : fun a ↦ a.fst ≤ k = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j : ℕ
rw : (∃ (b : ℕ) (a : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
rw [exists_comm]

Premises used: exists_comm
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j a b : ℕ
rw rw₁ : a + b = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ b + a = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j : ℕ
⊢ (∃ (b : ℕ) (a : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
exact exists₂_congr (fun a b ↦ by rw [add_comm])

Premises used: exists₂_congr
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
⊢ ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔
                      ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
rw :
  {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
rw [← map_prodComm_antidiagonal]

Premises used: Finset.map_prodComm_antidiagonal
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
simp_rw :
  map
      (({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
        (Equiv.prodComm ℕ ℕ).toEmbedding)
      (@antidiagonal _ Nat.instAddMonoid _ k) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]

Premises used: Finset.map_filter, Finset.Nat.antidiagonal_filter_snd_le_of_le, Finset.map_map
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
h₁ :
  ∀ (i j : ℕ),
    (i, j) ∈
        map
          (({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
            (Equiv.prodComm ℕ ℕ).toEmbedding)
          (@antidiagonal _ Nat.instAddMonoid _ k) ↔
      (i, j) ∈
        map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ k)
⊢ map
      (({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
        (Equiv.prodComm ℕ ℕ).toEmbedding)
      (@antidiagonal _ Nat.instAddMonoid _ k) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
ext ⟨i, j⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
i j : ℕ
⊢ (i, j) ∈
      map
        (({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
          (Equiv.prodComm ℕ ℕ).toEmbedding)
        (@antidiagonal _ Nat.instAddMonoid _ k) ↔
    (i, j) ∈
      map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ k)

Tactic:
simpa using aux₂ i j
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
h₁ :
  ∀ (i j : ℕ),
    (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.1} ↔
      (i, j) ∈
        map ({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (@antidiagonal _ Nat.instAddMonoid _ (n - k))
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.1} =
    map ({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
ext ⟨i, j⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
this : i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i
⊢ (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.1} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
simpa
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
h₁ : i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i
⊢ (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.1} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ (n - k))

Tactic:
suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i

Tactic:
⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩

Premises used: HSub.hSub, tsub_add_cancel_of_le, And.right, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
h₁ : ∀ (hi : i + j = n ∧ k ≤ i), i - k + j = n - k
h₂ : (∃ (a : ℕ), a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i
⊢ i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i

Tactic:
refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
h₁ : i + j - k = n - k
h₂ h₃ : n - k = n - k
⊢ i - k + j = n - k

Tactic:
rw [← Nat.sub_add_comm hi.2, hi.1]

Premises used: Nat.sub_add_comm, And.right, And.left
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k

Tactic:
⟨?_, Nat.le_add_left k l⟩

Premises used: Nat.le_add_left, And.intro
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
h₁ : l + k + j = n
⊢ l + k + j = n ∧ k ≤ l + k

Tactic:
refine ⟨?_, Nat.le_add_left k l⟩
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
h₁ : n - k + k = n
⊢ l + k + j = n

Tactic:
rw [add_right_comm, hl]

Premises used: add_right_comm
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n

Tactic:
tsub_add_cancel_of_le h

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ n - k + k = n

Tactic:
exact tsub_add_cancel_of_le h

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Data.Finset.NatAntidiagonal
Goal:
n k : ℕ
h : k ≤ n
⊢ Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))

Tactic:
have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl