kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @category_theory.induced_category.has_coe_to_sort ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @wide_subquiver_has_coe_to_sort ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_3 : has_coe_to_sort
  (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set.has_coe_to_sort ?x_11
failed is_def_eq

kbuzzard

import tactic
import data.real.basic
/-

# Some puzzles.

1) (easy logic). If `P`, `Q` and `R` are true-false statements, then show
that `(P → (Q → R)) → ((P → Q) → (P → R))` (where `→` means "implies")

2) (group theory) If `G` is a group such that `∀ g, g^2 = 1`

kbuzzard

⊢ @eq.{1} nat
    (@fintype.card.{u_2}
       (@alg_equiv.{u_1 u_2 u_2} F
          (@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
                (@intermediate_field.insert.insert.{u_2} E
                   (@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
                   (@intermediate_field.insert_empty.{u_2} E)
                   α)))

kbuzzard

key :
  @eq.{1} nat
    (@fintype.card.{u_2}
       (@alg_equiv.{u_1 u_2 u_2} F
          (@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
                (@intermediate_field.insert.insert.{u_2} E
                   (@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
                   (@intermediate_field.insert_empty.{u_2} E)

kbuzzard

import tactic

/-
Making group theory in a theorem prover
-/

namespace mygroup

-- A group needs multiplication, inverse, identity
class group (G : Type) extends has_mul G, has_inv G, has_one G :=

kbuzzard

-- boilerplate -- ignore for now
import tactic
import linear_algebra.finite_dimensional

open vector_space
open finite_dimensional
open submodule

-- Let's prove that if V is a 9-dimensional vector space, and X and Y are 5-dimensional subspaces
-- then X ∩ Y is non-zero

kbuzzard

# The list of topics was originally gathered from
# http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf

# 1.
Linear algebra:
  Fundamentals:
    vector space: 'algebra/module.html#vector_space'
    product of vector spaces: 'algebra/pi_instances.html#prod.module'
    vector subspace: 'algebra/module.html#subspace'
    quotient space: 'linear_algebra/basic.html#submodule.quotient'

kbuzzard

import tactic
import data.real.basic
/-

Fibonacci. Harder than it looks.

-/

def fib : ℕ → ℕ
| 0 := 0

kbuzzard

5,6c5,9
<        (@category_theory.functor.obj.{v v u u} C 𝒞 C 𝒞
<           (@category_theory.exp.functor.{v u} C 𝒞
---
>        (@category_theory.exp.{v u} C 𝒞
>           (@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
>           A
>           (@sheaf'.A.{v u} C 𝒞 _inst_1 _inst_2 j _inst_3 s)
>           (@category_theory.is_cartesian_closed.cart_closed.{v u} C 𝒞
8,13c11,12

kbuzzard

  @eq.{v+1}
    (@category_theory.has_hom.hom.{v u} C
       (@category_theory.category_struct.to_has_hom.{v u} C (@category_theory.category.to_category_struct.{v u} C 𝒞))
       B
       (@category_theory.exp.{v u} C 𝒞
          (@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
          A
          (@sheaf'.A.{v u} C 𝒞 _inst_1 _inst_2 j _inst_3 s)
          (@category_theory.is_cartesian_closed.cart_closed.{v u} C 𝒞
             (@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)