kbuzzard

c : ℕ,
h : c ≥ 3
⊢ c - 2 +
      int.nat_abs
        (2 +
           -↑(strong_induction_on 0
                  (λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
                   (L : multiset ℕ),
                     strong_induction_on L
                       (λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),

kbuzzard

0. [simplify.rewrite] [multiset.mem_singleton]: a ∈ c :: 0 ==> a = c
0. [simplify.rewrite] [ne.def]: c ≠ a ==> ¬c = a
0. [simplify.rewrite] [sub_eq_add_neg]: 2 - ↑(HC (erase C2 a) _ L2) ==> 2 + -↑(HC (erase C2 a) _ L2)
0. [simplify.rewrite] [sub_eq_add_neg]: 4 - ↑(HL (erase L2 a) _) ==> 4 + -↑(HL (erase L2 a) _)
0. [simplify.rewrite] [sub_eq_add_neg]: 2 -
  ↑(strong_induction_on (erase (c :: 0) a)
       (λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
          strong_induction_on L
            (λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
               N_min

kbuzzard

import data.finset
import algebra.big_operators
import data.fintype

open finset


lemma disjoint_equiv_classes (α : Type*) [fintype α] [h : setoid α] [decidable_rel h.r] [decidable_eq α]:
∀ x ∈ @finset.univ (quotient h) _, ∀ y ∈ @finset.univ (quotient h) _, x ≠ y → 
    (finset.filter (λ b : α, ⟦b⟧ = x) finset.univ) ∩ (finset.filter (λ b : α, ⟦b⟧ = y) finset.univ) = ∅ :=

kbuzzard

  @finset.sum.{0 ?l_1} nat (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3)
    (@add_comm_group.to_add_comm_monoid.{?l_1} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) ?m_4)
    (finset.range (@has_add.add.{0} nat nat.has_add k (@has_one.one.{0} nat nat.has_one)))
    (λ (i : nat),
       @has_mul.mul.{?l_1} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) ?m_5[i]
         (@has_pow.pow.{?l_1 0} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) nat ?m_6[i]
            (@mv_polynomial.C.{?l_1 0} ?m_2 nat (λ (a b : nat), nat.decidable_eq a b) ?m_7[i] ?m_3
               (@coe.{1 ?l_1+1} nat ?m_2 ?m_8[i] (@nat.Prime.p _inst_1)))
            i)
         (@has_pow.pow.{?l_1 0} (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) nat ?m_9[i]

kbuzzard

Pattern we're trying to rewrite:

  @finset.sum.{0 0} nat
    (@mv_polynomial.{0 0} nat rat
       (@comm_ring.to_comm_semiring.{0} rat
          (@nonzero_comm_ring.to_comm_ring.{0} rat
             (@integral_domain.to_nonzero_comm_ring.{0} rat
                (@field.to_integral_domain.{0} rat
                   (@linear_ordered_field.to_field.{0} rat
                      (@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat

kbuzzard

| @finset.sum.{0 0} nat
    (@mv_polynomial.{0 0} nat rat
       (@comm_ring.to_comm_semiring.{0} rat
          (@nonzero_comm_ring.to_comm_ring.{0} rat
             (@integral_domain.to_nonzero_comm_ring.{0} rat
                (@field.to_integral_domain.{0} rat
                   (@linear_ordered_field.to_field.{0} rat
                      (@discrete_linear_ordered_field.to_linear_ordered_field.{0} rat
                         rat.discrete_linear_ordered_field)))))))
    (@semiring.to_add_comm_monoid.{0}

kbuzzard

import data.set.basic tactic.interactive 
import data.list.basic 

-- todo -- there's some way of deriving decidable eq here I think
inductive square
| vampire : square
| ghost : square
| zombie : square 

namespace square

kbuzzard

failed to synthesize type class instance for
⊢ decidable
    (∃ (x : square),
       … ∧
         ∀ (y : square),
           (∃ (x : square),
              (∃ (x_1 : square),
                   … ∧
                     ∀ (y_1 : square),
                       (∃ (x_1 : square),

kbuzzard

The code that produced this trace was:

import ring_theory.ideals

set_option trace.class_instances true
def is_fg {α β} [ring α] [module α β]
  (s : set β) [is_submodule s] : Prop :=
∃ t : finset β, _root_.span (t : set β)  = s

at some point where there was a dodgy instance (since fixed). The error was a typeclass loop caused by line 8.

kbuzzard

/-
a + b = c and b + d = e -> c + d = a + e
-/

lemma nat.eq_sub_of_add {a b c : ℕ} (H : a + b = c) : c - b = a := by rw [←H,nat.add_sub_cancel]

lemma mod_eq_self_sub_div (a b : ℕ) : a % b = a - b * (a / b) := by rw nat.eq_sub_of_add (nat.mod_add_div a b)