awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
pos : count (x, y) (map (fun (x_1 : α) ↦ (x, x_1)) l) = count y l
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = count y l
have pos₁ : count y l = count y l
Tactic: rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0
have H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
Tactic: have H₁ {x y z : α} : count (x, y) (map (z, ·) l) = if z = x then count y l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
⊢ count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
have pos : ∀ (h : z = y), count (x, y) (map (fun (x : α) ↦ (x, z)) l) = count x l
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
pos : ∀ (h : z = y), count (x, y) (map (fun (x : α) ↦ (x, z)) l) = count x l
⊢ count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
have neg : ∀ (h : ¬z = y), count (x, y) (map (fun (x : α) ↦ (x, z)) l) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun (x : α) ↦ (x, z)) l) = count x l
have pos : count (x, y) (map (fun (x : α) ↦ (x, y)) l) = count x l
Tactic: rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
pos : count (x, y) (map (fun (x : α) ↦ (x, y)) l) = count x l
⊢ count (x, y) (map (fun (x : α) ↦ (x, z)) l) = count x l
have pos₁ : count x l = count x l
Tactic: rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0
have H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
Tactic: have H₂ {x y z : α} : count (x, y) (map (·, z) l) = if z = y then count x l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
⊢ count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0
have cons : ((if c = a then count b l else 0) + if c = b then count a l else 0) +
    (count a l * count b l - if a = b then count a l else 0) =
  (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
    if a = b then count a l + if c = a then 1 else 0 else 0
Tactic: simp only [(offDiag_cons_perm _ _).count_eq, count_append, ihl, H₁, H₂, count_cons, beq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have this : count c l ≤ count c l * count c l
Tactic: have := Nat.le_mul_self (count c l)
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have pos : c = a →
  c = b →
    a = b →
      count b l + count a l + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 1) - (count a l + 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have neg : c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
neg :
  c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have pos₁ : c = a →
  ¬c = b →
    a = b → count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
neg :
  c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
pos₁ :
  c = a →
    ¬c = b →
      a = b → count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have neg₁ : c = a → ¬c = b → ¬a = b → count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
neg :
  c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
pos₁ :
  c = a →
    ¬c = b →
      a = b → count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)
neg₁ : c = a → ¬c = b → ¬a = b → count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have pos₂ : ¬c = a →
  c = b →
    a = b → 0 + count a l + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 1) - (count a l + 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
neg :
  c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
pos₁ :
  c = a →
    ¬c = b →
      a = b → count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)
neg₁ : c = a → ¬c = b → ¬a = b → count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0
pos₂ :
  ¬c = a →
    c = b →
      a = b → 0 + count a l + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 1) - (count a l + 0)
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have neg₂ : ¬c = a → c = b → ¬a = b → 0 + count a l + (count a l * count b l - 0) = (count a l + 0) * (count b l + 1) - 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
neg :
  c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
pos₁ :
  c = a →
    ¬c = b →
      a = b → count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)
neg₁ : c = a → ¬c = b → ¬a = b → count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0
pos₂ :
  ¬c = a →
    c = b →
      a = b → 0 + count a l + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 1) - (count a l + 0)
neg₂ : ¬c = a → c = b → ¬a = b → 0 + count a l + (count a l * count b l - 0) = (count a l + 0) * (count b l + 1) - 0
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have pos₃ : ¬c = a →
  ¬c = b →
    a = b →
      HAdd.hAdd (α := ℕ) 0 0 + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 0) - (count a l + 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
pos :
  c = a →
    c = b →
      a = b →
        count b l + count a l + (count a l * count b l - count a l) =
          (count a l + 1) * (count b l + 1) - (count a l + 1)
neg :
  c = a → c = b → ¬a = b → count b l + count a l + (count a l * count b l - 0) = (count a l + 1) * (count b l + 1) - 0
pos₁ :
  c = a →
    ¬c = b →
      a = b → count b l + 0 + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)
neg₁ : c = a → ¬c = b → ¬a = b → count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0
pos₂ :
  ¬c = a →
    c = b →
      a = b → 0 + count a l + (count a l * count b l - count a l) = (count a l + 0) * (count b l + 1) - (count a l + 0)
neg₂ : ¬c = a → c = b → ¬a = b → 0 + count a l + (count a l * count b l - 0) = (count a l + 0) * (count b l + 1) - 0
pos₃ :
  ¬c = a →
    ¬c = b →
      a = b →
        HAdd.hAdd (α := ℕ) 0 0 + (count a l * count b l - count a l) =
          (count a l + 0) * (count b l + 0) - (count a l + 0)
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
have neg₃ : ¬c = a → ¬c = b → ¬a = b → HAdd.hAdd (α := ℕ) 0 0 + (count a l * count b l - 0) = (count a l + 0) * (count b l + 0) - 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h : c = a
h_1 : c = b
h_2 : a = b
⊢ count b l + count a l + (count a l * count b l - count a l) = (count a l + 1) * (count b l + 1) - (count a l + 1)
have pos : ∀ (ihl : count (b, b) l.offDiag = count b l * count b l - count b l)
  (H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0)
  (H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0)
  (this : count b l ≤ count b l * count b l),
  c = b →
    a = b →
      count b l + count b l + (count b l * count b l - count b l) = (count b l + 1) * (count b l + 1) - (count b l + 1)
Tactic: simp_all
Cleared hypotheses: ihl, H₁, H₂, this, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h : c = a
h_1 : ¬c = b
h_2 : ¬a = b
⊢ count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0
have neg : ∀ (ihl : count (a, b) l.offDiag = count a l * count b l)
  (H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0)
  (H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0)
  (this : count a l ≤ count a l * count a l),
  c = a → ¬a = b → count b l + count a l * count b l = (count a l + 1) * count b l
Tactic: simp_all
Cleared hypotheses: ihl, H₁, H₂, this, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
h : ¬c = a
h_1 : c = b
h_2 : ¬a = b
⊢ 0 + count a l + (count a l * count b l - 0) = (count a l + 0) * (count b l + 1) - 0
have neg : ∀ (ihl : count (a, b) l.offDiag = count a l * count b l)
  (H₁ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0)
  (H₂ : ∀ {x y z : α}, count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0)
  (this : count b l ≤ count b l * count b l),
  ¬b = a → c = b → ¬a = b → count a l + count a l * count b l = count a l * (count b l + 1)
Tactic: simp_all
Cleared hypotheses: ihl, H₁, H₂, this, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
⊢ count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
have nil : count (a, b) (offDiag []) = count a [] * count b [] - if a = b then count a [] else 0
Tactic: induction l with
  | nil => simp
  | cons c l ihl =>
    have H₁ {x y z : α} : count (x, y) (map (z, ·) l) = if z = x then count y l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    have H₂ {x y z : α} : count (x, y) (map (·, z) l) = if z = y then count x l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    simp only [(offDiag_cons_perm _ _).count_eq, count_append, ihl, H₁, H₂, count_cons, beq_iff_eq]
    have := Nat.le_mul_self (count c l)
    split_ifs <;> simp_all <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a b : α
nil : count (a, b) (offDiag []) = count a [] * count b [] - if a = b then count a [] else 0
⊢ count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
have cons : ∀ (c : α) (l : List α) (ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0),
  count (a, b) (c :: l).offDiag = count a (c :: l) * count b (c :: l) - if a = b then count a (c :: l) else 0
Tactic: induction l with
  | nil => simp
  | cons c l ihl =>
    have H₁ {x y z : α} : count (x, y) (map (z, ·) l) = if z = x then count y l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    have H₂ {x y z : α} : count (x, y) (map (·, z) l) = if z = y then count x l else 0 := by
      split_ifs with h
      · rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]
      · simp [count_eq_zero, h]
    simp only [(offDiag_cons_perm _ _).count_eq, count_append, ihl, H₁, H₂, count_cons, beq_iff_eq]
    have := Nat.le_mul_self (count c l)
    split_ifs <;> simp_all <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ l.offDiag.Nodup
have rw : ∀ (a : α × α), List.count a l.offDiag ≤ 1
Tactic: rw [nodup_iff_count_le_one]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ List.count (x, y) l.offDiag ≤ 1
have rw : (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1
Tactic: rw [count_offDiag_eq_mul_sub_ite l x y]
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
h : l.offDiag.Nodup
this : DecidableEq α := Classical.decEq α
⊢ l.Nodup
have simp : ∀ (h : ∀ (a b : α), (List.count a l * List.count b l - if a = b then List.count a l else 0) ≤ 1) (a : α),
  List.count a l ≤ 1
Tactic: simp only [nodup_iff_count_le_one, Prod.forall, count_offDiag_eq_mul_sub_ite] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
h : ∀ (a b : α), (List.count a l * List.count b l - if a = b then List.count a l else 0) ≤ 1
a : α
⊢ List.count a l ≤ 1
have h₁ : (List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
Tactic: specialize h a a
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (goal)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : (List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
⊢ List.count a l ≤ 1
have contrapose : ∀ (h : ¬List.count a l ≤ 1), ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.OffDiag (hypothesis)
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : ¬List.count a l ≤ 1
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
have h₁ : 1 < List.count a l
Tactic: rw [Nat.not_le] at h
Cleared hypotheses: h