ChrisHughes24

import Mathlib.Tactic

inductive E
| lit : Bool → E
| var : Nat → E
| ite : E → E → E → E
deriving DecidableEq

def E.hasNestedIf : E → Bool
| lit _ => false

ChrisHughes24

open Monoid Monoid.Coprod SemidirectProduct

-- def Monoid.CoprodI.mapEquivHom (ι M : Type*) [Monoid M] :
--     Equiv.Perm ι →* MulAut (Monoid.CoprodI (fun _ : ι => M)) :=
--   { toFun := fun e =>
--       MonoidHom.toMulEquiv
--         (Monoid.CoprodI.lift (fun i =>
--           CoprodI.of (M := fun _ : ι => M) (i := e i)))
--         (Monoid.CoprodI.lift (fun i =>
--           CoprodI.of (M := fun _ : ι => M) (i := e.symm i)))

ChrisHughes24

import Mathlib.GroupTheory.SemidirectProduct
import Mathlib.GroupTheory.FreeGroup

open FreeGroup SemidirectProduct Multiplicative

def freeAction : Multiplicative ℤ →* MulAut (FreeGroup (Multiplicative ℤ)) :=
  zpowersHom _ (freeGroupCongr (MulAction.toPermHom (Multiplicative ℤ)
    (Multiplicative ℤ) (ofAdd 1)))
#print mint
example : FreeGroup Bool ≃*

ChrisHughes24

import order.zorn
import category_theory.category.preorder
import category_theory.limits.cones

universes u v w

namespace category_theory

open limits

ChrisHughes24

inductive AccT {α : Type u} (r : α → α → Sort v) : α → Type (max u v) where
  | intro (x : α) (h : (y : α) → r y x → AccT r y) : AccT r x

namespace AccT

def inv {x y : α} : (h₁ : AccT r x) → (h₂ : r y x) → AccT r y
| ⟨_, h⟩, h₂ => h y h₂

def NatAccT : (n : Nat) → @AccT Nat (. < .) n
| 0 => AccT.intro 0 (fun y h => (Nat.not_lt_zero y h).elim)

ChrisHughes24

universe u

inductive EQ {α : Type u} (a : α) : α → Type
| refl : EQ a

def casT {α β : Type} (h : EQ α β) (a : α) : β :=
@EQ.rec_on Type α (λ A hA, A) β h a

def EQ.trans {α : Type u} {a b c : α} (h₁ : EQ a b) (h₂ : EQ b c) : EQ a c :=
@EQ.rec_on α b (λ A hA, EQ a A) c h₂ h₁

ChrisHughes24

import data.mv_polynomial.variables
import field_theory.is_alg_closed.basic
import data.finset.lattice
import data.zmod.basic

noncomputable theory

/-- the data of a polynomial map consists of n polynomials in n variables -/
@[simp] def poly_map (K : Type*) [comm_semiring K] (n : ℕ) : Type* :=
fin n → mv_polynomial (fin n) K

ChrisHughes24

import tactic

variables (P : Type) [partial_order P]

def presheaf : Type :=
{ s : P → Prop // ∀ a b, a ≤ b → s b → s a }

instance : has_coe_to_fun (presheaf P) (λ _, P → Prop) :=
⟨subtype.val⟩

ChrisHughes24

import linear_algebra.finsupp

variables {R α M N P : Type} [comm_ring R] [add_comm_group M] [module R M]
variables [add_comm_group N] [module R N]
variables [add_comm_group P] [module R P]

noncomputable theory

namespace poly_example

ChrisHughes24

import data.set.function
import data.fintype.basic
import data.finset.basic
import data.fin
import tactic

open finset function

@[derive fintype, derive decidable_eq]
structure cell := (r : fin 9) (c : fin 9)