awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
x : ℕ × ℕ
rw : x ∈ (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) ↔ x.1 + x.2 = n
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n
have rw₁ : x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
Tactic: rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
x : ℕ × ℕ
rw : x ∈ (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) ↔ x.1 + x.2 = n
rw₁ : x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n
have rw₂ : x.1 + x.2 = n ↔ x.1 + x.2 = n
Tactic: rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ (antidiagonal n).card = n + 1
have rw : (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)).card = n + 1
Tactic: rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)).card = n + 1
⊢ (antidiagonal n).card = n + 1
have rw₁ : (List.Nat.antidiagonal n).length = n + 1
Tactic: rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)).card = n + 1
rw₁ : (List.Nat.antidiagonal n).length = n + 1
⊢ (antidiagonal n).card = n + 1
have rw₂ : n + 1 = n + 1
Tactic: rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₁ : (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₂ : (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) + (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₃ : (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) + (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₃ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₄ : (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) + (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₃ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₄ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₅ : (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) + (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₃ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₄ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₅ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₆ : (↑([(n + 1, 0)] ++ List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₃ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₄ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₅ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
rw₆ :
  (↑([(n + 1, 0)] ++ List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₇ : (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
  (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : (↑(List.Nat.antidiagonal (n + 1)) : Multiset (ℕ × ℕ)) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₁ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₂ :
  (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) +
      (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₃ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
rw₄ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₅ :
  (↑[(n + 1, 0)] : Multiset (ℕ × ℕ)) +
      (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
rw₆ :
  (↑([(n + 1, 0)] ++ List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
rw₇ :
  (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
    (n + 1, 0) ::ₘ (↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
⊢ antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
have rw₈ : (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) =
  (↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
have rw : (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
  (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
Tactic: rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ map Prod.swap (antidiagonal n) = antidiagonal n
have rw : map Prod.swap (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : map Prod.swap (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
⊢ map Prod.swap (antidiagonal n) = antidiagonal n
have rw₁ : (↑(List.map Prod.swap (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : map Prod.swap (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₁ :
  (↑(List.map Prod.swap (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
⊢ map Prod.swap (antidiagonal n) = antidiagonal n
have rw₂ : (↑(List.Nat.antidiagonal n).reverse : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : map Prod.swap (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₁ :
  (↑(List.map Prod.swap (List.Nat.antidiagonal n)) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
rw₂ : (↑(List.Nat.antidiagonal n).reverse : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
⊢ map Prod.swap (antidiagonal n) = antidiagonal n
have rw₃ : (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) = (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ))
Tactic: rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) ≍ cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f)
have apply : ∀ (a_1 a'_1 : α),
  a_1 ≍ a'_1 →
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a_1 ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'_1
Tactic: apply hfunext rfl
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
⊢ ∀ (a_1 a'_1 : α),
    a_1 ≍ a'_1 →
      cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a_1 ≍
        cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'_1
have simp : ∀ (a_1 a'_1 : α),
  a_1 = a'_1 →
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a_1 ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'_1
Tactic: simp only [heq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ (a'' ∈ a ::ₘ a' ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)
have rw : (a'' ∈ a' ::ₘ a ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)
Tactic: rw [Multiset.cons_swap]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ≍ cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a''
have refine : ∀ (ha₁ : a'' ∈ a ::ₘ a' ::ₘ m) (ha₂ : a'' ∈ a' ::ₘ a ::ₘ m),
  ha₁ ≍ ha₂ →
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
Tactic: refine hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
have inl : ∀ (h₁ : a'' ≠ a),
  cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
Tactic: rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
inl :
  ∀ (h₁ : a'' ≠ a),
    cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
have inr : ∀ {b : δ a''} (h : a'' ≠ a') (ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m) (ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m),
  ha₁ ≍ ha₂ →
    cons (δ := δ) (a' ::ₘ m) a'' b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
      cons (δ := δ) (a'' ::ₘ m) a' b' (cons (δ := δ) m a'' b f) a'' ha₂
Tactic: rcases Decidable.ne_or_eq a'' a with (h₁ | rfl)
Cleared hypotheses: a, b, h, ha₁, ha₂, h_1
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
have inl : ∀ {b' : δ a''} (h : a ≠ a'') (ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m) (ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m),
  ha₁ ≍ ha₂ →
    cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂
Tactic: rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
Cleared hypotheses: a', b', h, ha₁, ha₂, h_1
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
inl :
  ∀ {b' : δ a''} (h : a ≠ a'') (ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m) (ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m),
    ha₁ ≍ ha₂ →
      cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
        cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
have inl₁ : ∀ (h₂ : a'' ≠ a'),
  cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
Tactic: rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
have inl : ∀ {b' : δ a''} (h : a ≠ a'') (ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m) (ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m),
  ha₁ ≍ ha₂ →
    cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
      cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂
Tactic: on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
Cleared hypotheses: a', b', h, ha₁, ha₂, h_1
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
h_1 : ha₁ ≍ ha₂
h₁ : a'' ≠ a
inl :
  ∀ {b' : δ a''} (h : a ≠ a'') (ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m) (ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m),
    ha₁ ≍ ha₂ →
      cons (δ := δ) (a'' ::ₘ m) a b (cons (δ := δ) m a'' b' f) a'' ha₁ ≍
        cons (δ := δ) (a ::ₘ m) a'' b' (cons (δ := δ) m a b f) a'' ha₂
⊢ cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
have inl₁ : ∀ (h₂ : a'' ≠ a'),
  cons (δ := δ) (a' ::ₘ m) a b (cons (δ := δ) m a' b' f) a'' ha₁ ≍
    cons (δ := δ) (a ::ₘ m) a' b' (cons (δ := δ) m a b f) a'' ha₂
Tactic: on_goal 1 => rcases Decidable.eq_or_ne a'' a' with (rfl | h₂)
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
⊢ (cons (δ := δ) m a (f a ⋯) fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) = f
have h : ∀ (a' : α) (h' : a' ∈ a ::ₘ m), cons (δ := δ) m a (f a sorry) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' sorry) a' h' = f a' h'
Tactic: ext a' h'
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
have pos : ∀ (h : a' = a), cons (δ := δ) m a (f a sorry) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' sorry) a' h' = f a' h'
Tactic: by_cases h : a' = a
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
pos : ∀ (h : a' = a), cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
have neg : ∀ (h : ¬a' = a), cons (δ := δ) m a (f a sorry) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' sorry) a' h' = f a' h'
Tactic: by_cases h : a' = a
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
have pos : ∀ (f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1) (h' : a' ∈ a' ::ₘ m),
  cons (δ := δ) m a' (f a' sorry) (fun (a'_1 : α) (ha' : a'_1 ∈ m) ↦ f a'_1 sorry) a' h' = f a' h'
Tactic: subst h
Cleared hypotheses: a, f, h', h