350 lines of mathlib defs in a self-contained file so I could debug an issue

MWE

universe u

set_option old_structure_cmd true

/- 0,+ -/
class add_zero_class (M : Type u) extends has_zero M, has_add M :=
(zero_add : ∀ (a : M), 0 + a = a)
(add_zero : ∀ (a : M), a + 0 = a)

class add_semigroup (G : Type u) extends has_add G :=
(add_assoc : ∀ a b c : G, a + b + c = a + (b + c))

class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M.

class add_comm_semigroup (G : Type u) extends add_semigroup G :=
(add_comm : ∀ a b : G, a + b = b + a)

class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M

/- 1,* -/

class mul_one_class (M : Type u) extends has_one M, has_mul M :=
(one_mul : ∀ (a : M), 1 * a = a)
(mul_one : ∀ (a : M), a * 1 = a)

class semigroup (G : Type u) extends has_mul G :=
(mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))

class comm_semigroup (G : Type u) extends semigroup G :=
(mul_comm : ∀ a b : G, a * b = b * a)

def npow_rec {M : Type*} [has_one M] [has_mul M] : ℕ → M → M
| 0     a := 1
| (n+1) a := a * npow_rec n a

class monoid (M : Type u) extends semigroup M, mul_one_class M :=
(npow : ℕ → M → M := npow_rec)

class comm_monoid (M : Type u) extends monoid M, comm_semigroup M

instance monoid.has_pow {M : Type u} [monoid M] : has_pow M ℕ := ⟨λ x n, monoid.npow n x⟩

/- 0 1 * -/

class mul_zero_class (M₀ : Type*) extends has_mul M₀, has_zero M₀ :=
(zero_mul : ∀ a : M₀, 0 * a = 0)
(mul_zero : ∀ a : M₀, a * 0 = 0)

class semigroup_with_zero (S₀ : Type*) extends semigroup S₀, mul_zero_class S₀.

class mul_zero_one_class (M₀ : Type*) extends mul_one_class M₀, mul_zero_class M₀.

class monoid_with_zero (M₀ : Type*) extends monoid M₀, mul_zero_one_class M₀.

/- 0 1 + * -/

class distrib (R : Type*) extends has_mul R, has_add R :=
(left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c))
(right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c))

class non_unital_non_assoc_semiring (α : Type u) extends
  add_comm_monoid α, distrib α, mul_zero_class α

class non_unital_semiring (α : Type u) extends
  non_unital_non_assoc_semiring α, semigroup_with_zero α

class non_assoc_semiring (α : Type u) extends
  non_unital_non_assoc_semiring α, mul_zero_one_class α

class semiring (α : Type u) extends non_unital_semiring α, non_assoc_semiring α, monoid_with_zero α

class comm_semiring (α : Type u) extends semiring α, comm_monoid α

/- Morphisms -/

structure zero_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] :=
(to_fun : M → N)
(map_zero' : to_fun 0 = 0)

structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] :=
(to_fun : M → N)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

structure add_monoid_hom (M : Type*) (N : Type*) [add_zero_class M] [add_zero_class N]
  extends zero_hom M N, add_hom M N

structure one_hom (M : Type*) (N : Type*) [has_one M] [has_one N] :=
(to_fun : M → N)
(map_one' : to_fun 1 = 1)

structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

structure monoid_hom (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N]
  extends one_hom M N, mul_hom M N

structure monoid_with_zero_hom (M : Type*) (N : Type*) [mul_zero_one_class M] [mul_zero_one_class N]
  extends zero_hom M N, monoid_hom M N

structure ring_hom (α : Type*) (β : Type*) [semiring α] [semiring β]
  extends monoid_hom α β, add_monoid_hom α β, monoid_with_zero_hom α β

infixr ` →+* `:25 := ring_hom

instance ring_hom.has_coe_to_fun {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} :
  has_coe_to_fun (α →+* β) := ⟨_, ring_hom.to_fun⟩

def ring_hom.id (α : Type*) [semiring α] : α →+* α :=
{ to_fun := id,
  map_zero' := sorry,
  map_one' := sorry,
  map_add' := sorry,
  map_mul' := sorry }


def ring_hom.comp {α β γ : Type*} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ}
  (hnp : β →+* γ) (hmn : α →+* β) : α →+* γ :=
{ to_fun := hnp ∘ hmn,
  map_zero' := sorry,
  map_one' := sorry,
  map_add' := sorry,
  map_mul' := sorry }

/- subobjects -/

structure add_submonoid (M : Type*) [add_zero_class M] :=
(carrier : set M)
(zero_mem' : (0 : M) ∈ carrier)
(add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier)

structure submonoid (M : Type*) [mul_one_class M] :=
(carrier : set M)
(one_mem' : (1 : M) ∈ carrier)
(mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier)

structure subsemiring (R : Type u) [semiring R] extends submonoid R, add_submonoid R

/- nat and facts -/

class fact (p : Prop) : Prop := (out [] : p)

def nat.prime (p : ℕ) := 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p

protected def nat.cast {α : Type*} [has_zero α] [has_one α] [has_add α] : ℕ → α
| 0     := 0
| (n+1) := nat.cast n + 1

@[priority 900] instance nat.cast_coe {α : Type*} [_inst_1 : has_zero α] [_inst_2 : has_one α]
  [_inst_3 : has_add α] : has_coe_t ℕ α := ⟨nat.cast⟩

class char_p (R : Type*) [add_monoid R] [has_one R] (p : ℕ) : Prop :=
(cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)

/- Pi -/

namespace pi
universes v
variable {I : Type u}     -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances
variables (x y : Π i, f i) (i : I)

instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩
instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ _, 0⟩
instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ f g i, f i + g i⟩
instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩
instance mul_one_class [∀ i, mul_one_class $ f i] : mul_one_class (Π i : I, f i) :=
{ one := (1 : Π i, f i), mul := (*), one_mul := sorry, mul_one := sorry }

instance semiring [∀ i, semiring $ f i] : semiring (Π i : I, f i) :=
{ zero := (0 : Π i, f i), one := 1, add := (+), mul := (*),
  add_assoc := sorry,
  zero_add := sorry,
  add_zero := sorry,
  add_comm := sorry,
  left_distrib := sorry,
  right_distrib := sorry,
  zero_mul := sorry,
  mul_zero := sorry,
  mul_assoc := sorry,
  one_mul := sorry,
  mul_one := sorry,
}

instance comm_semiring [∀ i, comm_semiring $ f i] : comm_semiring (Π i : I, f i) :=
{ zero := (0 : Π i, f i), one := 1, add := (+), mul := (*),
  add_assoc := sorry,
  zero_add := sorry,
  add_zero := sorry,
  add_comm := sorry,
  left_distrib := sorry,
  right_distrib := sorry,
  zero_mul := sorry,
  mul_zero := sorry,
  mul_assoc := sorry,
  one_mul := sorry,
  mul_one := sorry,
  mul_comm := sorry }


end pi

/- setlike -/

class set_like (A : Type*) (B : out_param $ Type*) :=
(coe : A → set B)
(coe_injective' : function.injective coe)

instance submonoid.set_like {M : Type*} [mul_one_class M] : set_like (submonoid M) M :=
⟨submonoid.carrier, sorry⟩

instance add_submonoid.set_like {M : Type*} [add_zero_class M] : set_like (add_submonoid M) M :=
⟨add_submonoid.carrier, sorry⟩

instance subsemiring.set_like {R : Type*} [semiring R] : set_like (subsemiring R) R :=
⟨subsemiring.carrier, sorry⟩

namespace set_like

variables {A : Type*} {B : Type*} [i : set_like A B]

include i

instance : has_coe_t A (set B) := ⟨set_like.coe⟩

@[priority 100]
instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩

-- `dangerous_instance` does not know that `B` is used only as an `out_param`
instance : has_coe_to_sort A := ⟨_, λ p, {x : B // x ∈ p}⟩

end set_like

/- coercion from subobject to object -/

theorem subtype.coe_injective {α : Type*} {p : α → Prop}  :
  function.injective (coe : subtype p → α) := sorry

protected def function.injective.add_semigroup {M₁ : Type*} {M₂ : Type*} [has_add M₁] [add_semigroup M₂]
  (f : M₁ → M₂) (hf : function.injective f)
  (add : ∀ x y, f (x + y) = f x + f y) :
  add_semigroup M₁ :=
{ add_assoc := sorry,
  ..‹has_add M₁› }

protected def function.injective.semigroup {M₁ : Type*} {M₂ : Type*} [has_mul M₁] [semigroup M₂] (f : M₁ → M₂)
  (hf : function.injective f)
  (mul : ∀ x y, f (x * y) = f x * f y) :
  semigroup M₁ :=
{ mul_assoc := sorry,
  ..‹has_mul M₁› }

protected def function.injective.add_comm_semigroup {M₁ : Type*} {M₂ : Type*} [has_add M₁]
  [add_comm_semigroup M₂] (f : M₁ → M₂) (hf : function.injective f)
  (add : ∀ x y, f (x + y) = f x + f y) :
  add_comm_semigroup M₁ :=
{ add_comm := sorry,
  .. hf.add_semigroup f add }


protected def function.injective.add_zero_class {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁]
  [add_zero_class M₂] (f : M₁ → M₂) (hf : function.injective f)
  (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) :
  add_zero_class M₁ :=
{ zero_add := sorry,
  add_zero := sorry,
  ..‹has_zero M₁›, ..‹has_add M₁› }

protected def function.injective.mul_one_class {M₁ : Type*} {M₂ : Type*} [has_one M₁] [has_mul M₁] [mul_one_class M₂] (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  mul_one_class M₁ :=
{ one_mul := sorry,
  mul_one := sorry,
  ..‹has_one M₁›, ..‹has_mul M₁› }

protected def function.injective.add_monoid {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁] [add_monoid M₂]
  (f : M₁ → M₂) (hf : function.injective f)
  (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) :
  add_monoid M₁ :=
{ .. hf.add_semigroup f add, .. hf.add_zero_class f zero add }

protected def function.injective.monoid {M₁ : Type*} {M₂ : Type*} [has_one M₁] [has_mul M₁] [monoid M₂]
  (f : M₁ → M₂) (hf : function.injective f)
  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
  monoid M₁ :=
{ .. hf.semigroup f mul, .. hf.mul_one_class f one mul }

protected def function.injective.add_comm_monoid {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁]
  [add_comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f)
  (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) :
  add_comm_monoid M₁ :=
{ .. hf.add_comm_semigroup f add, .. hf.add_monoid f zero add }


instance add_submonoid.has_zero {M : Type*} [add_zero_class M] (S : add_submonoid M): has_zero S := ⟨⟨0, sorry⟩⟩
instance submonoid.has_one {M : Type*} [mul_one_class M] (S : submonoid M): has_one S := ⟨⟨1, sorry⟩⟩
instance submonoid.has_add {M : Type*} [add_zero_class M] (S : add_submonoid M): has_add S := ⟨λ a b, ⟨a.1 + b.1, sorry⟩⟩
instance submonoid.has_mul {M : Type*} [mul_one_class M] (S : submonoid M): has_mul S := ⟨λ a b, ⟨a.1 * b.1, sorry⟩⟩

instance submonoid.to_monoid {M : Type*} [monoid M] (S : submonoid M) : monoid S :=
subtype.coe_injective.monoid coe sorry sorry

instance add_submonoid.to_add_comm_monoid {M} [add_comm_monoid M] (S : add_submonoid M) : add_comm_monoid S :=
subtype.coe_injective.add_comm_monoid coe rfl (λ _ _, rfl)

instance subsemiring.to_semiring {R : Type u} [semiring R] (s : subsemiring R) : semiring s :=
{ mul_zero := sorry,
  zero_mul := sorry,
  right_distrib := sorry,
  left_distrib := sorry,
  .. s.to_submonoid.to_monoid, .. s.to_add_submonoid.to_add_comm_monoid }

instance subsemiring.to_comm_semiring {R} [comm_semiring R] (s : subsemiring R) : comm_semiring s :=
{ mul_comm := sorry, ..s.to_semiring}

/- char p ring theory -/

def monoid.perfection (M : Type*) [comm_monoid M] (p : ℕ) : submonoid (ℕ → M) :=
{ carrier := { f | ∀ n, f (n + 1) ^ p = f n },
  one_mem' := sorry,
  mul_mem' := sorry }

def ring.perfection (R : Type*) [comm_semiring R]
  (p : ℕ) [hp : fact p.prime] [char_p R p] :
  subsemiring (ℕ → R) :=
{ zero_mem' := sorry,
  add_mem' := sorry,
  .. monoid.perfection R p }

instance char_p.subsemiring (R : Type u) [semiring R] (p : ℕ) [char_p R p] (S : subsemiring R) :
  char_p S p := ⟨sorry⟩

instance char_p.pi (ι : Type u) [hi : nonempty ι] (R : Type*) [semiring R] (p : ℕ) [char_p R p] :
  char_p (ι → R) p := ⟨sorry⟩

def frobenius (R : Type*) [comm_semiring R] (p : ℕ) [fact p.prime] [char_p R p] : R →+* R :=
{ to_fun := λ x, x^p,
  map_one' := sorry,
  map_mul' := sorry,
  map_zero' := sorry,
  map_add' := sorry }

def perfection.coeff (R : Type*) [comm_semiring R] (p : ℕ) [hp : fact (nat.prime p)]
  [_inst_2 : char_p R p] (n : ℕ) : ring.perfection R p →+* R :=
{ to_fun := λ f, f.1 n,
  map_one' := rfl,
  map_mul' := λ f g, rfl,
  map_zero' := rfl,
  map_add' := λ f g, rfl }

/-- The `p`-th root of an element of the perfection. -/
def pth_root (R : Type*) [comm_semiring R] (p : ℕ) [hp : fact (nat.prime p)] [char_p R p] :
  ring.perfection R p →+* ring.perfection R p :=
{ to_fun := λ f, ⟨λ n, perfection.coeff R p (n + 1) f, λ n, f.2 _⟩,
  map_one' := rfl,
  map_mul' := λ f g, rfl,
  map_zero' := rfl,
  map_add' := λ f g, rfl }

lemma frobenius_pth_root {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
  (frobenius (ring.perfection R p) p).comp (pth_root R p) = ring_hom.id (ring.perfection R p) :=
sorry

-- Type* not Type u causes timeout
lemma frobenius_pth_root_bad {R : Type*} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] :
  (frobenius (ring.perfection R p) p).comp (pth_root R p) = ring_hom.id (ring.perfection R p) :=
sorry