awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (hypothesis)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)
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
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])
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
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
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)
have rw : {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | a.1 ≤ k} =
  map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := sorry : ℕ ↪ ℕ })
    (@antidiagonal _ Nat.instAddMonoid _ k)
Tactic: rw [← map_prodComm_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
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
⊢ {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)
have simp_rw : map
    (({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := sorry : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
      (Equiv.prodComm ℕ ℕ).toEmbedding)
    (@antidiagonal _ Nat.instAddMonoid _ k) =
  map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := sorry : ℕ ↪ ℕ })
    (@antidiagonal _ Nat.instAddMonoid _ k)
Tactic: simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
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
⊢ 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)
have h₁ : ∀ (i j : ℕ),
  (i, j) ∈
      map
        (({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := sorry : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
          (Equiv.prodComm ℕ ℕ).toEmbedding)
        (@antidiagonal _ Nat.instAddMonoid _ k) ↔
    (i, j) ∈
      map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := sorry : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ k)
Tactic: ext ⟨i, j⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.1} =
    map ({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
have h₁ : ∀ (i j : ℕ),
  (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.1} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + k, inj' := sorry : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ (n - k))
Tactic: ext ⟨i, j⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
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))
have h₁ : i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i
Tactic: suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i
have h₁ : ∀ (hi : i + j = n ∧ k ≤ i), i - k + j = n - k
Tactic: refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
h₁ : ∀ (hi : i + j = n ∧ k ≤ i), i - k + j = n - k
⊢ i + j = n ∧ k ≤ i ↔ ∃ (a : ℕ), a + j = n - k ∧ a + k = i
have h₂ : (∃ (a : ℕ), a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i
Tactic: refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
⊢ i - k + j = n - k
have h₁ : i + j - k = n - k
Tactic: rw [← Nat.sub_add_comm hi.2, hi.1]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ k ≤ i
h₁ : i + j - k = n - k
⊢ i - k + j = n - k
have h₂ : n - k = n - k
Tactic: rw [← Nat.sub_add_comm hi.2, hi.1]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n ∧ k ≤ l + k
have h₁ : l + k + j = n
Tactic: refine ⟨?_, Nat.le_add_left k l⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n
have h₁ : n - k + k = n
Tactic: rw [add_right_comm, hl]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (hypothesis)
Goal:
n k : ℕ
h : k ≤ n
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
have aux₁ : 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
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j : ℕ
⊢ (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
have rw : (∃ (b : ℕ) (a : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
Tactic: rw [exists_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j a b : ℕ
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j
have rw : a + b = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (hypothesis)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
have aux₂ : ∀ (i j : ℕ),
  (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
Tactic: have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
                      ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
have rw : {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | k ≤ a.2} =
  map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := sorry : ℕ ↪ ℕ })
    (@antidiagonal _ Nat.instAddMonoid _ (n - k))
Tactic: rw [← map_prodComm_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
⊢ {a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (@antidiagonal _ AddCommMonoid.toAddMonoid _ n) | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
have simp_rw : map
    (({ toFun := fun (x : ℕ) ↦ x + k, inj' := sorry : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
      (Equiv.prodComm ℕ ℕ).toEmbedding)
    (@antidiagonal _ Nat.instAddMonoid _ (n - k)) =
  map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := sorry : ℕ ↪ ℕ })
    (@antidiagonal _ Nat.instAddMonoid _ (n - k))
Tactic: simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ k ≤ a.2)
    ((fun (a : ℕ × ℕ) ↦ k ≤ a.1) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
aux₂ :
  ∀ (i j : ℕ),
    (∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = n - k ∧ a = i ∧ b + k = j
⊢ map
      (({ toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
        (Equiv.prodComm ℕ ℕ).toEmbedding)
      (@antidiagonal _ Nat.instAddMonoid _ (n - k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ (n - k))
have h₁ : ∀ (i j : ℕ),
  (i, j) ∈
      map
        (({ toFun := fun (x : ℕ) ↦ x + k, inj' := sorry : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)).trans
          (Equiv.prodComm ℕ ℕ).toEmbedding)
        (@antidiagonal _ Nat.instAddMonoid _ (n - k)) ↔
    (i, j) ∈
      map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + k, inj' := sorry : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ (n - k))
Tactic: ext ⟨i, j⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
x : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i) ∈ @antidiagonal _ Nat.instAddMonoid _ n
have rw : i ≤ n
Tactic: rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ ∃ (j : α),
    (∀ d < j, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
      LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) j : ℕ) ((single a 1 : (a : α) → ℕ) j : ℕ)
have h₁ : (∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
  LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
Tactic: use a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ (∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
    LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
have h₁ : ∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Lex (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
h₁ : ∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)
⊢ (∀ d < a, Eq (α := ℕ) ((single b 1 : (a : α) → ℕ) d : ℕ) ((single a 1 : (a : α) → ℕ) d : ℕ)) ∧
    LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
have h₂ : LT.lt (α := ℕ) ((single b 1 : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a b : σ →₀ ℕ
⊢ (m.toSyn : (a : σ →₀ ℕ) → m.syn) a ≤
    HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) b : m.syn)
have rw : LE.le.{u_2} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (a + b) : m.syn)
Tactic: rw [← map_add]
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_2} σ
a : m.syn
⊢ 0 ≤ a
have this : (m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 ≤
  HAdd.hAdd (α := m.syn) (β := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) a) : m.syn)
Tactic: have := m.le_add_right 0 (m.toSyn.symm a)
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder (goal)
Goal:
⊢ GT.gt (α := Lex (ℕ →₀ ℕ)) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2) : Lex (ℕ →₀ ℕ))
    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (HAdd.hAdd (α := ℕ →₀ ℕ) (single 0 1) (single 1 1)) : Lex (ℕ →₀ ℕ))
have h : (∀ (j : ℕ),
    (fun (x1 x2 : ℕ) ↦ x1 < x2) j 0 →
      Eq (α := (@fun {i : ℕ} ↦ ℕ) j)
        ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ)
                  ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (HAdd.hAdd (α := ℕ →₀ ℕ) (single 0 1) (single 1 1))) :
                ℕ →₀ ℕ) :
              (a : ℕ) → ℕ)
            j :
          ℕ)
        ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
              (a : ℕ) → ℕ)
            j :
          ℕ)) ∧
  (@fun {i : ℕ} (x1 x2 : ℕ) ↦ x1 < x2) 0
    ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ)
            ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (HAdd.hAdd (α := ℕ →₀ ℕ) (single 0 1) (single 1 1))) :
          ℕ →₀ ℕ) :
        (a : ℕ) → ℕ)
      0)
    ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
        (a : ℕ) → ℕ)
      0)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder (goal)
Goal:
⊢ LT.lt (α := Lex (ℕ →₀ ℕ)) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1) : Lex (ℕ →₀ ℕ))
    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 1) : Lex (ℕ →₀ ℕ))
have h : (∀ (j : ℕ),
    (fun (x1 x2 : ℕ) ↦ x1 < x2) j 0 →
      Eq (α := (@fun {i : ℕ} ↦ ℕ) j)
        ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
              (a : ℕ) → ℕ)
            j :
          ℕ)
        ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 1)) : ℕ →₀ ℕ) :
              (a : ℕ) → ℕ)
            j :
          ℕ)) ∧
  (@fun {i : ℕ} (x1 x2 : ℕ) ↦ x1 < x2) 0
    ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
        (a : ℕ) → ℕ)
      0)
    ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 1)) : ℕ →₀ ℕ) :
        (a : ℕ) → ℕ)
      0)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.MonomialOrder (goal)
Goal:
⊢ LT.lt (α := Lex (ℕ →₀ ℕ)) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1) : Lex (ℕ →₀ ℕ))
    ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2) : Lex (ℕ →₀ ℕ))
have h : (∀ (j : ℕ),
    (fun (x1 x2 : ℕ) ↦ x1 < x2) j 0 →
      Eq (α := (@fun {i : ℕ} ↦ ℕ) j)
        ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
              (a : ℕ) → ℕ)
            j :
          ℕ)
        ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
              (a : ℕ) → ℕ)
            j :
          ℕ)) ∧
  (@fun {i : ℕ} (x1 x2 : ℕ) ↦ x1 < x2) 0
    ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 1 1)) : ℕ →₀ ℕ) :
        (a : ℕ) → ℕ)
      0)
    ((((ofLex : (a : Lex (ℕ →₀ ℕ)) → ℕ →₀ ℕ) ((toLex : (a : ℕ →₀ ℕ) → Lex (ℕ →₀ ℕ)) (single 0 2)) : ℕ →₀ ℕ) :
        (a : ℕ) → ℕ)
      0)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
⊢ (↑(f.neLocus g) : Set α) = {x : α | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)}
have h : ∀ (x : α),
  x ∈ (↑(f.neLocus g) : Set α) ↔
    Membership.mem (γ := Set α) {x : α | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
⊢ f.neLocus g = g.neLocus f
have simp_rw : {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} =
  {x ∈ g.support ∪ f.support | Ne.{u_3 + 1} (α := N) ((g : (a : α) → N) x : N) ((f : (a : α) → N) x : N)}
Tactic: simp_rw [neLocus, Finset.union_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f g : α →₀ N
simp_rw :
  {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} =
    {x ∈ g.support ∪ f.support | Ne.{u_3 + 1} (α := N) ((g : (a : α) → N) x : N) ((f : (a : α) → N) x : N)}
⊢ f.neLocus g = g.neLocus f
have simp_rw₁ : {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) x : N) ((g : (a : α) → N) x : N)} =
  {x ∈ f.support ∪ g.support | Ne.{u_3 + 1} (α := N) ((g : (a : α) → N) x : N) ((f : (a : α) → N) x : N)}
Tactic: simp_rw [neLocus, Finset.union_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
⊢ f.neLocus 0 = f.support
have h : ∀ (a : α), a ∈ f.neLocus 0 ↔ a ∈ f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
a : α
⊢ a ∈ f.neLocus 0 ↔ a ∈ f.support
have h : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔ a ∈ f.support
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
a : α
h : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔ a ∈ f.support
⊢ a ∈ f.neLocus 0 ↔ a ∈ f.support
have h₁ : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔
  Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
a : α
h : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔ a ∈ f.support
h₁ :
  Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔
    Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
⊢ a ∈ f.neLocus 0 ↔ a ∈ f.support
have h₂ : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 a : N) ↔ Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero N
f : α →₀ N
a : α
h : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔ a ∈ f.support
h₁ :
  Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) ((0 : (a : α) → N) a : N) ↔
    Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
h₂ : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 a : N) ↔ Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
⊢ a ∈ f.neLocus 0 ↔ a ∈ f.support
have h₃ : Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N) ↔ Ne.{u_3 + 1} (α := N) ((f : (a : α) → N) a : N) (0 : N)
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : Zero M
inst_3 : DecidableEq P
inst_4 : Zero P
inst_5 : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective.{u_3 + 1, u_4 + 1} (β := P) fun (g : N) ↦ F f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂
have h : ∀ (a : α), a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : DecidableEq α
inst_1 : DecidableEq M
inst_2 : Zero M
inst_3 : DecidableEq P
inst_4 : Zero P
inst_5 : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective.{u_2 + 1, u_4 + 1} (β := P) fun (f : M) ↦ F f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂
have h : ∀ (a : α), a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : DecidableEq M
inst_3 : Zero M
inst_4 : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g
have h : ∀ (a : α), a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ (-f).neLocus g = f.neLocus (-g)
have rw : (- -f).neLocus (-g) = f.neLocus (-g)
Tactic: rw [← neLocus_neg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
rw : (- -f).neLocus (-g) = f.neLocus (-g)
⊢ (-f).neLocus g = f.neLocus (-g)
have rw₁ : f.neLocus (-g) = f.neLocus (-g)
Tactic: rw [← neLocus_neg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.NeLocus (goal)
Goal:
α : Type u_1
N : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq N
inst_2 : AddGroup N
f g : α →₀ N
⊢ f.neLocus g = (f - g).support
have rw : (f + -g).neLocus (g + -g) = (f - g).support
Tactic: rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]