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.functor.obj.{v v u u} C 𝒞 C 𝒞
          (@category_theory.exp.functor.{v u} C 𝒞
             (@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
             A
             (@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)

kbuzzard

import tactic
/-!

Order of the subgroup divides order of the group, from first principles,
with proofs written in tactic mode.

Just so kmb can see how long the proof is. Can we teach it?

-/

kbuzzard

empty_perfectoid : @subtype.{2} CLVRS
  (λ (X : CLVRS),
     is_perfectoid
       (@subtype.mk.{1} nat (λ (p : nat), nat.prime p) (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))
          nat.prime_two)
       X) :=
  @subtype.mk.{2} CLVRS
    (λ (X : CLVRS),
       is_perfectoid
         (@subtype.mk.{1} nat (λ (p : nat), nat.prime p) (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))

kbuzzard

def empty_perfectoid : PerfectoidSpace
  (@subtype.mk.{1} nat (λ (p : nat), nat.prime p)
     (@bit1.{0} nat nat.has_one nat.has_add
        (@bit0.{0} nat nat.has_add
           (@bit1.{0} nat nat.has_one nat.has_add
              (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))))))
     empty_perfectoid._proof_1) :=
@subtype.mk.{2} CLVRS
  (λ (X : CLVRS),
     is_perfectoid

kbuzzard

[type_context.is_def_eq] Sort ? =?= Prop ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ... success  (approximate mode)
[type_context.is_def_eq] Type =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := ℂ
[type_context.is_def_eq_detail] assign: ?m_1 := ℂ
[type_context.is_def_eq] ?m_1 =?= ℂ ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := complex.nondiscrete_normed_field
[type_context.is_def_eq_detail] [1]: nondiscrete_normed_field ?m_1 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq_detail] [2]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] assign: ?m_1 := complex.nondiscrete_normed_field

kbuzzard

[type_context.is_def_eq] Sort ? =?= Prop ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ... success  (approximate mode)
[type_context.is_def_eq] Type =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := ℂ
[type_context.is_def_eq_detail] assign: ?m_1 := ℂ
[type_context.is_def_eq] ?m_1 =?= ℂ ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := complex.nondiscrete_normed_field
[type_context.is_def_eq_detail] [1]: nondiscrete_normed_field ?m_1 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq_detail] [2]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] assign: ?m_1 := complex.nondiscrete_normed_field

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @pi.semimodule ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)
  (@add_comm_group.to_add_comm_monoid (β → α)
     (@pi.add_comm_group β (λ (a : β), α) (λ (i : β), @ring.to_add_comm_group α _inst_1))) := @add_comm_monoid.nat_semimodule ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_0 : @semimodule α (β → α) (@ring.to_semiring α _inst_1)

kbuzzard

[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Sort ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: Type ? =?= subalgebra ?m_1 ?m_2

kbuzzard

import group.definitions -- definition of a group

namespace mygroup

variables {G : Type} [group G] -- let G be a group

/- 

Axioms for a group:

kbuzzard

/-
Copyright (c) 2020 Shing Tak Lam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shing Tak Lam
-/

import tactic
import data.polynomial

/-!