ChrisHughes24

/-
Copyright (c) 2019 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
-/
import data.matrix data.pequiv data.rat.basic

namespace pequiv
open matrix

ChrisHughes24

set_option old_structure_cmd true

class has_coe_to_fun' (Γ dom cod : Type) :=
( to_fun : Γ → dom → cod )

instance has_coe_to_fun'.has_coe_to_fun (Γ α β : Type) [has_coe_to_fun' Γ α β] : 
  has_coe_to_fun Γ := ⟨_, @has_coe_to_fun'.to_fun _ α β _⟩

structure add_group_hom (α β : Type) [add_group α] [add_group β] :=
( to_fun : α → β )

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) 

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

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 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 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.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 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 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})