digama0

import Mathlib.Tactic.NormNum
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.SlimCheck

namespace Tactic

namespace Approx

def RoundDown (a b : ℤ) : Prop := 2 * b ≤ a
#align tactic.approx.round_down Tactic.Approx.RoundDown

digama0

// [dependencies]
// metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.7" }
// rand = "0.8"

use metamath_knife::{statement::StatementAddress, verify::ProofBuilder, Database, StatementType};
use rand::Rng;
use std::collections::{hash_map::RandomState, HashMap, HashSet};
use std::ops::Range;

struct Pass<'a>(&'a HashMap<StatementAddress, u32>, &'a mut AccessSeq);

digama0

import set_theory.cofinality
import order.symm_diff
import group_theory.subgroup.basic
import group_theory.group_action.basic

noncomputable theory
open_locale cardinal classical

universes u v

digama0

// [package]
// name = "breen-deligne-homology"
// version = "0.1.0"
// authors = ["Mario Carneiro <di.gama@gmail.com>"]
// edition = "2018"

// [dependencies]
// modinverse = "0.1"
// rand = "0.8"

digama0

import Lean.Elab.Tactic

def findLeast (a : Array Nat) : Nat := do
  let mut smallest := a[0]
  for i in [1:a.size] do
    if a[i] ≤ smallest then
      smallest := a[i]
  return smallest

#eval findLeast #[8, 3, 10, 4, 6]

digama0

import tactic.rcases
/-
The problem is originally presented in:
A. Pease, G. Sutcliffe, N. Siegel, and S. Trac, “Large Theory
Reasoning with SUMO at CASC,” pp. 1–8, Jul. 2009.
Here we present the natural deduction proof in Lean.
-/

constant U : Type

digama0

import tactic.norm_num
import algebra.group_power
open prod
universes u v w ℓ

inductive let_bound (α : Type*)
| base : α → let_bound
| dlet : ℤ → (ℤ → let_bound) → let_bound
| mlet {β : Type} : β → (β → let_bound) → let_bound
open let_bound

digama0

/-
  Presheaf (of types).
  https://stacks.math.columbia.edu/tag/006D
-/

import topology.basic
import topology.opens
import order.bounds

digama0

import data.fintype algebra.ordered_field

theorem multiset.inj_of_nodup_map {α β} (f : α → β) {s : multiset α} (h : (multiset.map f s).nodup)
  {x y} (h₁ : x ∈ s) (h₂ : y ∈ s) (e : f x = f y) : x = y :=
begin
  rcases multiset.exists_cons_of_mem h₁ with ⟨s, rfl⟩,
  cases multiset.mem_cons.1 h₂, {exact h_1.symm},
  simp only [multiset.map_cons, multiset.nodup_cons, multiset.mem_map] at h,
  cases h.1 ⟨_, h_1, e.symm⟩
end

digama0

*** The goal today is to prove the following theorem:

h50::itexp.1         |- ( ph -> A e. RR )
h51::itexp.2         |- ( ph -> B e. RR )
h52::itexp.3         |- ( ph -> A <_ B )
h53::itexp.4       |- ( ph -> N e. NN )
qed::              |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )

*** Jon thinks it would be easier to do this without the "ph ->", but I think he may regret that decision later.
*** Anyway it is epsilon harder to have a context so let's just go with it.