awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
x y : α
⊢ (x, y) ∈ l.offDiag ↔
    ∃ (i : ℕ),
      ∃ (x_1 : i < l.length),
        ∃ (j : ℕ),
          ∃ (x_2 : j < l.length),
            i ≠ j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x_1 = (x, y).fst ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j x_2 = (x, y).snd

Tactic:
simp only [offDiag, exists_mem_zipIdx, mem_eraseIdx_iff_getElem, mem_flatMap, mem_map,
    Nat.zero_add, Prod.ext_iff, ← exists_and_right, exists_and_left, @exists_comm α, and_assoc,
    exists_eq_left', ne_comm]

Premises used: List.mem_eraseIdx_iff_getElem, Prod.ext_iff, exists_and_left, exists_eq_left', List.offDiag, exists_and_right, exists_comm, and_assoc, ne_comm, List.exists_mem_zipIdx, List.mem_flatMap, Nat.zero_add, List.mem_map
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
⊢ count (a, b) (offDiag []) = count a [] * count b [] - if a = b then count a [] else 0

Tactic:
simp
-- Module: Mathlib.Data.List.OffDiag
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 : α
pos : ∀ (h : z = x), count (x, y) (map (fun (x : α) ↦ (z, x)) l) = count y l
neg : ∀ (h : ¬z = x), count (x, y) (map (fun (x : α) ↦ (z, x)) l) = 0
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = if z = x then count y l else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.OffDiag
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
⊢ Function.Injective (β := α × α) fun (x_1 : α) ↦ (x, x_1)

Tactic:
simp [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Data.List.OffDiag
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
pos₁ pos₂ : count y l = count y l
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = count y l

Tactic:
rw [h, count_map_of_injective l (x, ·) (by simp [Function.Injective])]

Premises used: Prod.mk, List.count_map_of_injective
-- Module: Mathlib.Data.List.OffDiag
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
⊢ count (x, y) (map (fun (x : α) ↦ (z, x)) l) = 0

Tactic:
simp [count_eq_zero, h]

Premises used: List.count_eq_zero
-- Module: Mathlib.Data.List.OffDiag
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 : α}, 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]
-- Module: Mathlib.Data.List.OffDiag
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
neg : ∀ (h : ¬z = y), count (x, y) (map (fun (x : α) ↦ (x, z)) l) = 0
⊢ count (x, y) (map (fun (x : α) ↦ (x, z)) l) = if z = y then count x l else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.OffDiag
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
⊢ Function.Injective (β := α × α) fun (x : α) ↦ (x, y)

Tactic:
simp [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Data.List.OffDiag
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
pos₁ pos₂ : count x l = count x l
⊢ count (x, y) (map (fun (x : α) ↦ (x, z)) l) = count x l

Tactic:
rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]

Premises used: Prod.mk, List.count_map_of_injective
-- Module: Mathlib.Data.List.OffDiag
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) = 0

Tactic:
simp [count_eq_zero, h]

Premises used: List.count_eq_zero
-- Module: Mathlib.Data.List.OffDiag
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

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]
-- Module: Mathlib.Data.List.OffDiag
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
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
⊢ 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:
simp only [(offDiag_cons_perm _ _).count_eq, count_append, ihl, H₁, H₂, count_cons, beq_iff_eq]

Premises used: beq_iff_eq, List.count_cons, List.count_append, List.Perm.count_eq, List.offDiag_cons_perm
-- Module: Mathlib.Data.List.OffDiag
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 c l ≤ count c l * count c l

Tactic:
have := Nat.le_mul_self (count c l)
-- Module: Mathlib.Data.List.OffDiag
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)
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
⊢ ((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:
split_ifs
-- Module: Mathlib.Data.List.OffDiag
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
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)
⊢ 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:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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 - 0) = (count a l + 1) * (count b l + 1) - 0

Tactic:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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 - count a l) = (count a l + 1) * (count b l + 0) - (count a l + 1)

Tactic:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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
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
⊢ count b l + 0 + (count a l * count b l - 0) = (count a l + 1) * (count b l + 0) - 0

Tactic:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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 - count a l) = (count a l + 0) * (count b l + 1) - (count a l + 0)

Tactic:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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
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)
⊢ 0 + count a l + (count a l * count b l - 0) = (count a l + 0) * (count b l + 1) - 0

Tactic:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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
⊢ 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:
simp_all
-- Module: Mathlib.Data.List.OffDiag
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
⊢ HAdd.hAdd (α := ℕ) 0 0 + (count a l * count b l - 0) = (count a l + 0) * (count b l + 0) - 0

Tactic:
simp_all
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
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
h : c = b
h_1 : 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:
grind
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
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
h : c = a
h_1 : ¬a = b
⊢ count b l + count a l * count b l = (count a l + 1) * count b l

Tactic:
grind
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
inst : DecidableEq α
a b c : α
l : List α
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
h : ¬b = a
h_1 : c = b
h_2 : ¬a = b
⊢ count a l + count a l * count b l = count a l * (count b l + 1)

Tactic:
grind
-- Module: Mathlib.Data.List.OffDiag
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
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
⊢ count (a, b) l.offDiag = count a l * count b l - if a = b then count a 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

Premises used: beq_iff_eq, List.count_cons, List.cons, List.count_append, List.Perm.count_eq, List.offDiag_cons_perm, List.nil
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁.offDiag ~ l₂.offDiag

Tactic:
simp_all [perm_iff_count, count_offDiag_eq_mul_sub_ite]

Premises used: List.count_offDiag_eq_mul_sub_ite, List.perm_iff_count
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁.offDiag ~ l₂.offDiag

Tactic:
classical simp_all [perm_iff_count, count_offDiag_eq_mul_sub_ite]

Premises used: List.count_offDiag_eq_mul_sub_ite, List.perm_iff_count
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
rw : ∀ (a : α × α), List.count a l.offDiag ≤ 1
⊢ l.offDiag.Nodup

Tactic:
rw [nodup_iff_count_le_one]

Premises used: List.nodup_iff_count_le_one
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
rw : (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1
⊢ List.count (x, y) l.offDiag ≤ 1

Tactic:
rw [count_offDiag_eq_mul_sub_ite l x y]

Premises used: List.count_offDiag_eq_mul_sub_ite
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1

Tactic:
grind
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.offDiag.Nodup
this : DecidableEq α := Classical.decEq α
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
⊢ l.Nodup

Tactic:
simp only [nodup_iff_count_le_one, Prod.forall, count_offDiag_eq_mul_sub_ite] at *

Premises used: List.count_offDiag_eq_mul_sub_ite, Prod.forall, List.nodup_iff_count_le_one
-- Module: Mathlib.Data.List.OffDiag
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 * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
specialize h a a
-- Module: Mathlib.Data.List.OffDiag
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
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
⊢ List.count a l ≤ 1

Tactic:
contrapose h
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : ¬List.count a l ≤ 1
⊢ 1 < List.count a l

Tactic:
rw [Nat.not_le] at h

Premises used: Nat.not_le
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this_1 : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
this : 1 + List.count a l < List.count a l * List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
simpa
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
suffices : 1 + List.count a l < List.count a l * List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
suffices 1 + l.count a < l.count a * l.count a by simpa
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 1 + List.count a l < List.count a l + List.count a l

Tactic:
simpa
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
rw : 2 * List.count a l ≤ List.count a l * List.count a l
⊢ List.count a l + List.count a l ≤ List.count a l * List.count a l

Tactic:
rw [← Nat.two_mul]

Premises used: Nat.two_mul
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 2 * List.count a l ≤ List.count a l * List.count a l

Tactic:
Nat.mul_le_mul_right _ h

Premises used: Nat.mul_le_mul_right
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 2 * List.count a l ≤ List.count a l * List.count a l

Tactic:
exact Nat.mul_le_mul_right _ h

Premises used: Nat.mul_le_mul_right
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
a₁ : 1 + List.count a l < List.count a l + List.count a l
a₂ : List.count a l + List.count a l ≤ List.count a l * List.count a l
⊢ 1 + List.count a l < List.count a l * List.count a l

Tactic:
calc
    1 + l.count a < l.count a + l.count a := by simpa
    _ ≤ l.count a * l.count a := by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h

Premises used: List.count
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
⊢ l.offDiag.Nodup ↔ l.Nodup

Tactic:
⟨.of_offDiag, .offDiag⟩

Premises used: List.Nodup.of_offDiag, List.Nodup.offDiag, Iff.intro
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
x : α × α
rcases : ∀ (x y : α), (x, y) ∈ l.offDiag ↔ (x, y).fst ∈ l ∧ (x, y).snd ∈ l ∧ (x, y).fst ≠ (x, y).snd
⊢ x ∈ l.offDiag ↔ x.fst ∈ l ∧ x.snd ∈ l ∧ x.fst ≠ x.snd

Tactic:
rcases x with ⟨x, y⟩
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
x y : α
simp_rw :
  (∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y) ↔
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
⊢ (x, y) ∈ l.offDiag ↔ (x, y).fst ∈ l ∧ (x, y).snd ∈ l ∧ (x, y).fst ≠ (x, y).snd

Tactic:
simp_rw [mem_offDiag_iff_getElem, mem_iff_getElem, Ne]

Premises used: Ne, List.mem_offDiag_iff_getElem, List.mem_iff_getElem