ChrisHughes24

import logic.function.iterate
import tactic

def h : (ℕ → bool) → bool × (ℕ → bool) :=
λ s, (s 0, s ∘ nat.succ)

variables {X : Type} (f : X → bool × X)

def UMP (x : X) (n : ℕ) : bool :=
(f ((prod.snd ∘ f)^[n] x)).1

ChrisHughes24

variables
  (formula : Type) 
  (T_proves : formula → Prop) 
  (provable : formula → formula)
  (implies : formula → formula → formula)
  (himplies : ∀ {φ ψ}, T_proves (implies φ ψ) → T_proves φ → T_proves ψ)
  (and : formula → formula → formula)
  (handl : ∀ {φ ψ}, T_proves (and φ ψ) → T_proves φ)
  (handr : ∀ {φ ψ}, T_proves (and φ ψ) → T_proves ψ)
  (false : formula)

ChrisHughes24

import group_theory.semidirect_product
import group_theory.free_group

open free_group multiplicative semidirect_product

universes u v

def free_group_hom_ext {α G : Type*} [group G] {f g : free_group α →* G}
  (h : ∀ a : α, f (of a) = g (of a)) (w : free_group α) : f w = g w :=
free_group.induction_on w (by simp) h (by simp) (by simp {contextual := tt})

ChrisHughes24

import tactic

inductive word₀
| blank : word₀
| concat : word₀ → word₀ → word₀

open word₀
infixr ` □ `:80 := concat

@[simp] lemma ne_concat_self_left : ∀ u v, u ≠ u □ v

ChrisHughes24

import data.equiv.basic data.option.basic
import tactic
universe u

axiom weak_univalence {α β : Sort*} : α ≃ β → α = β

def propext2 {p q : Prop} (h : p ↔ q) : p = q :=
weak_univalence ⟨h.mp, h.mpr, λ _, rfl, λ _, rfl⟩

section propext_free

ChrisHughes24

import analysis.special_functions.trigonometric

open complex real

example (θ φ : ℝ) (h1 : θ ≤ pi) (h2 : -pi < θ)
  (h3 : 0 < cos φ): arg (exp (I * θ) * cos φ) = θ :=
by rw [mul_comm, ← of_real_cos, arg_real_mul _ h3, mul_comm, exp_mul_I,  
    arg_cos_add_sin_mul_I h2 h1]

ChrisHughes24

import data.dfinsupp
import tactic

universes u v w

variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, decidable_eq (β i j)]
variables [Π i j, has_zero (β i j)] 

def to_fun (x : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j :=

ChrisHughes24

import data.nat.digits

lemma nat.div_lt_of_le : ∀ {n m k : ℕ} (h0 : n > 0) (h1 : m > 1) (hkn : k ≤ n), k / m < n
| 0     m k h0 h1 hkn := absurd h0 dec_trivial
| 1     m 0 h0 h1 hkn := by rwa nat.zero_div
| 1     m 1 h0 h1 hkn :=
  have ¬ (0 < m ∧ m ≤ 1), from λ h, absurd (@lt_of_lt_of_le ℕ 
    (show preorder ℕ, from @partial_order.to_preorder ℕ (@linear_order.to_partial_order ℕ nat.linear_order))
     _ _ _ h1 h.2) dec_trivial,
  by rw [nat.div_def_aux, dif_neg this]; exact dec_trivial

ChrisHughes24

import algebra.group.basic data.buffer

universe u

@[derive decidable_eq, derive has_reflect] inductive group_term : Type
| of : ℕ → group_term
| one : group_term
| mul : group_term → group_term → group_term
| inv : group_term → group_term

ChrisHughes24

prelude
import init.logic
set_option old_structure_cmd true

universe u

class comm_semigroup (α : Type u) extends has_mul α

class monoid (α : Type u) extends has_mul α, has_one α :=
(one_mul : ∀ a : α, 1 * a = a)