import Mathlib.Algebra.Category.Grp.Basic
import Mathlib.Algebra.Ring.BooleanRing
import Mathlib.Data.Nat.PSub
import Mathlib.NumberTheory.Harmonic.ZetaAsymp
import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

/-!
Here we collect some uniquely type-theoretic junk theorems. Let's warm up with a couple of basic
ones:
**Theorem 1.** The third coordinate of the rational number `1 / 2` is a bijection.
-/
theorem one_half_third_coord_is_bijection : Function.Bijective (1 / 2 : ℚ).3 := by
  constructor
  · simp [Function.Injective]
  · simp [Function.Surjective]

/-!
**Theorem 2.**
The first coordinate of the polynomial `X^2 * (X^3 + X + 1)` is equal to the prime
factorization of `30`.
-/
theorem polynomial_factorization_30 :
    (Polynomial.X^2 * (Polynomial.X^3 + Polynomial.X + 1)).1 = (30).factorization := by
  have h : (.X^2 : Polynomial ℕ) * (.X^3 + .X + 1) = .X^2 + .X^3 + .X^5 := by ring
  rw [h]
  have : Finsupp.single 2 1 + Finsupp.single 3 1 + Finsupp.single 5 1 = Nat.factorization 30 := by
    have h2 : 30 = 2 * 3 * 5 := by ring
    have f2 : Finsupp.single 2 1 = (2).factorization := by rw [Nat.Prime.factorization]; decide
    have f3 : Finsupp.single 3 1 = (3).factorization := by rw [Nat.Prime.factorization]; decide
    have f5 : Finsupp.single 5 1 = (5).factorization := by rw [Nat.Prime.factorization]; decide
    rw [h2, Nat.factorization_mul, Nat.factorization_mul]
    · simp_all only [Nat.reduceMul]
    all_goals simp
  simp_all only [Polynomial.toFinsupp_add, Polynomial.toFinsupp_X_pow]

/-!
For the next theorem, we will need a large number of lemmas. I legitimately do not know if this is
necessary, since it's just a computation involving some polynomials.
-/
lemma poly_1 : (Polynomial.X^2 + Polynomial.X + Polynomial.C 1 : Polynomial ℕ)
    = Polynomial.ofFinsupp (Finsupp.single 0 1 + Finsupp.single 1 1 + Finsupp.single 2 1) := by
  have e0 : (.C 1) = Polynomial.ofFinsupp (Finsupp.single 0 1) := by abel
  have e1 : (.X : Polynomial ℕ) = Polynomial.ofFinsupp (Finsupp.single 1 1) := by abel
  have e2 : (.X^2 : Polynomial ℕ) = Polynomial.ofFinsupp (Finsupp.single 2 1) := by
    simp_all only [Polynomial.ofFinsupp_single, Polynomial.monomial_zero_left, eq_natCast,
    Nat.cast_one, Polynomial.monomial_pow, one_mul, one_pow]
  rw [Polynomial.ofFinsupp_add,Polynomial.ofFinsupp_add]
  simp_all only [Polynomial.ofFinsupp_single, Polynomial.monomial_zero_left, eq_natCast,
    Nat.cast_one, Polynomial.monomial_pow, one_mul, one_pow]
  abel

lemma poly_2 : (MvPolynomial.X 0 + MvPolynomial.X 1 + MvPolynomial.X 2)^3 =
    ( (.X 0)^3
    + (.X 1)^3
    + (.X 2)^3
    + (.C 3)*(.X 0)^2*(.X 1)
    + (.C 3)*(.X 0)^2*(.X 2)
    + (.C 3)*(.X 1)^2*(.X 0)
    + (.C 3)*(.X 1)^2*(.X 2)
    + (.C 3)*(.X 2)^2*(.X 0)
    + (.C 3)*(.X 2)^2*(.X 1)
    + (.C 6)*(.X 0)*(.X 1)*(.X 2) : MvPolynomial ℕ ℕ) := by
  simp only [eq_natCast, Nat.cast_ofNat]; ring_nf

lemma poly_3 (n m : ℕ) : (.X n : MvPolynomial ℕ ℕ)^m
  = .monomial (.single n m) 1 := by exact MvPolynomial.X_pow_eq_monomial

lemma poly_4 (c n k : ℕ) : (.C c)*(.X n)^2*(.X k)
  = MvPolynomial.monomial (.single n 2 + .single k 1) c := by
  rw [MvPolynomial.X_pow_eq_monomial, MvPolynomial.C_mul_monomial, mul_one]
  unfold MvPolynomial.X; simp only [MvPolynomial.monomial_mul, mul_one]

lemma poly_5 (c : ℕ) : (.C c)*(.X 0)*(.X 1)*(.X 2)
  = MvPolynomial.monomial (.single 0 1 + .single 1 1 + .single 2 1) c := by
  unfold MvPolynomial.X; rw [MvPolynomial.C_mul_monomial]
  simp only [mul_one, MvPolynomial.monomial_mul]

lemma poly_6 : (.X 0 + .X 1 + .X 2)^3 =
     .monomial (.single 0 3) 1
   + .monomial (.single 1 3) 1
   + .monomial (.single 2 3) 1
   + .monomial (.single 0 2 + .single 1 1) 3
   + .monomial (.single 0 2 + .single 2 1) 3
   + .monomial (.single 1 2 + .single 0 1) 3
   + .monomial (.single 1 2 + .single 2 1) 3
   + .monomial (.single 2 2 + .single 0 1) 3
   + .monomial (.single 2 2 + .single 1 1) 3
   + MvPolynomial.monomial (.single 0 1 + .single 1 1 + .single 2 1) 6 := by
   rw [poly_2,poly_3,poly_3,poly_3,poly_4,poly_4,poly_4,poly_4,poly_4,poly_4,poly_5]

lemma poly_7 (A B : MvPolynomial ℕ ℕ) : (A + B).2 = A.2 + B.2 := by trivial

lemma poly_8 (n : ℕ) : (MvPolynomial.monomial (.single n 3) 1).2
  = Finsupp.single (.single n 3) 1 := by abel

lemma poly_9 (n m : ℕ) :
  (.monomial (.single n 2 + .single m 1) 3 : MvPolynomial ℕ ℕ).2
    = Finsupp.single (.single n 2 + .single m 1) 3 := by abel

lemma poly_10 : (.monomial (.single 0 1 + .single 1 1 + .single 2 1) 6 : MvPolynomial ℕ ℕ).2
    = (.single (.single 0 1 + .single 1 1 + .single 2 1) 6 : Finsupp (Finsupp ℕ ℕ) ℕ) := by abel

lemma poly_11 : ((.X 0 + .X 1 + .X 2)^3 : MvPolynomial ℕ ℕ).2 =
  (.single (.single 0 3) 1
 + .single (.single 1 3) 1
 + .single (.single 2 3) 1
 + .single (.single 0 2 + .single 1 1) 3
 + .single (.single 0 2 + .single 2 1) 3
 + .single (.single 1 2 + .single 0 1) 3
 + .single (.single 1 2 + .single 2 1) 3
 + .single (.single 2 2 + .single 0 1) 3
 + .single (.single 2 2 + .single 1 1) 3
 + .single (.single 0 1 + .single 1 1 + .single 2 1) 6
   : Finsupp (Finsupp ℕ ℕ) ℕ) := by simp [poly_6,poly_7,poly_8,poly_9,poly_10]

/-!
**Theorem 3. ** Let `P` be the multivariate polynomial `(X_0 + X_1 + X_2)^3`. Let `Q` be the
univariate polynomial `X^2 + X + 1`. The second coordinate of `P` applied to the first coordinate
of `Q` is equal to the natural number `6`.
-/
theorem polynomials_within_polynomials : ((.X 0 + .X 1 + .X 2)^3
    : MvPolynomial _ _).2 (.X^2 + .X + .C 1 : Polynomial _).1 = 6 := by
  rw [poly_1, poly_11]
  simp only [Finsupp.coe_add, Pi.add_apply, Finsupp.single_eq_same, Nat.add_eq_right,
  Nat.add_eq_zero_iff, Finsupp.single_apply, Finsupp.ext_iff, ite_eq_right_iff, one_ne_zero,
  imp_false, not_forall, Finsupp.coe_add, Pi.add_apply, OfNat.ofNat_ne_zero, add_left_inj]
  refine ⟨⟨⟨⟨⟨⟨⟨⟨⟨0,?_⟩,⟨1,?_⟩⟩,⟨2,?_⟩⟩,⟨0,?_⟩⟩,⟨0,?_⟩⟩,⟨1,?_⟩⟩,⟨0,?_⟩⟩,⟨2,?_⟩⟩,⟨2,?_⟩⟩
  all_goals intro h; simp at h
  all_goals rw [Finsupp.add_apply, Finsupp.add_apply] at h
  all_goals simp at h

lemma Prop.isOpen_iff (X : Set Prop) : IsOpen X ↔ X = ∅ ∨ X = {⊤} ∨ X = Set.univ := by
  apply Iff.intro
  · intro h; induction h
    · right; left; grind
    · right; right; rfl
    all_goals grind
  · intro h; apply Or.elim h
    · intro h2; rw [h2]; simp
    · intro h2; apply Or.elim h2
      all_goals (intro h3; rw [h3]; simp)

/-!
**Theorem 4.** The set `{z : ℝ | z ≠ 0}` is a continuous, non-monotone surjection.
-/
theorem set_of_nonzero_reals_is_continuous_nonmono_surjection :
       Continuous {z : ℝ | z ≠ 0}
    ∧ ¬Monotone {z : ℝ | z ≠ 0}
    ∧  Function.Surjective {z : ℝ | z ≠ 0} := by
  repeat' constructor
  · intro s h; rw [Prop.isOpen_iff] at h; apply Or.elim h
    · intro h2; rw [h2]; simp
    · intro h2; apply Or.elim h2
      · intro h3; rw [h3]; unfold setOf; simp [isOpen_ne]
      · intro h3; rw [h3]; simp
  · intro h
    have h1 : -1 ≤ (0 : ℝ) := by norm_num
    apply h at h1; simp [setOf] at h1
  · intro a; by_cases a
    · use 1; simp [setOf]; tauto
    · use 0; simp [setOf]; tauto

lemma Prop.isClosed_iff (X : Set Prop) : IsClosed X ↔ X = ∅ ∨ X = {⊥} ∨ X = Set.univ := by
  apply Iff.intro
  · intro h
    have h2 : IsOpen Xᶜ := by simp_all only [isOpen_compl_iff]
    rw [isOpen_iff] at h2; apply Or.elim h2
    · intro h3; right; right; rw [<- compl_eq_comm,eq_comm] at h3; rw [h3]; grind
    · intro h3; apply Or.elim h3
      · intro h4; right; left; rw [compl_eq_comm,eq_comm] at h4; rw [h4]; simp
      · intro h4; left; rw [compl_eq_comm,eq_comm] at h4; rw [h4]; simp
  · intro h; rw [<- compl_compl X, isClosed_compl_iff]; apply Or.elim h
    · intro h2; rw [h2,isOpen_iff]; simp
    · intro h2; apply Or.elim h2
      · intro h3; rw [h3,isOpen_iff]; simp
      · intro h3; rw [h3,isOpen_iff]; simp

lemma Prop.closure_singleton_true_univ : closure ({⊤} : Set Prop) = Set.univ := by
  unfold closure; ext; rw [Set.mem_sInter]; apply Iff.intro
  · simp
  · intro h X h2
    have h3 : IsClosed X := by grind
    have h4 : {⊤} ⊆ X := by grind
    rw [isClosed_iff] at h3; apply Or.elim h3
    · intro h5; rw [h5] at h4; tauto
    · intro h5; apply Or.elim h5
      · intro h6; rw [h6] at h4; rw [Set.singleton_subset_singleton] at h4
        by_contra; tauto
      · intro h6; rw [h6]; simp

/-!
**Theorem 5.** The Riemann hypothesis is in the topological closure of the set not not.
-/
theorem Riemann_hypothesis_in_closure_of_not_not : RiemannHypothesis ∈ closure (¬¬ ·) := by
  have h3 : (¬¬ ·) = ({⊤} : Set Prop) := by
    unfold Not singleton Set.instSingletonSet Set.singleton; aesop
  rw [h3,Prop.closure_singleton_true_univ]; simp

/-!
**Theorem 6.** The following are equivalent: The binary expansion of `7`.
-/
theorem TFAE_7_binary : List.TFAE (7).bits := by
  unfold Nat.bits Nat.binaryRec Nat.binaryRec; simp!

/-!
**Theorem 7.** The dot product of not with itself. Moreover, the matrix determinant of or. However,
not the determinant of and.
-/
theorem not_dot_not_det_or_and_not_det_and : dotProduct not not
                                          ∧  Matrix.det or
                                          ∧ ¬Matrix.det and := by decide

/-!
The next theorem will require by far the longest proof because it actually is a specific case of a
fairly nontrivial fact. I apologize for my amateurish proofs (in general but especially here).
-/
lemma Set_instMeasurableSpace_generatedFrom {A : Type u} :
    Set.instMeasurableSpace
    = (MeasurableSpace.generateFrom {{X | a ∈ X} | a : A} : MeasurableSpace (Set A)) := by
  unfold Set.instMeasurableSpace inferInstance MeasurableSpace.pi
  rw [MeasurableSpace.measurableSpace_iSup_eq, id]; apply LE.le.antisymm
  · apply MeasurableSpace.generateFrom_le; intro t h; simp only at t; apply Set.mem_setOf.1 at h
    cases h with
    | intro Y h =>
      unfold MeasurableSet MeasurableSpace.comap at h
      simp only [MeasurableSpace.measurableSet_top, true_and] at h
      cases h with
      | intro Z h2 => cases (Classical.em _ : True ∈ Z ∨ True ∉ Z) with
        | inl h3 => cases (Classical.em _ : False ∈ Z ∨ False ∉ Z) with
          | inl h4 =>
            have : Z = .univ := by
              ext P; constructor
              · grind
              · intro h5
                have : P = True ∨ P = False := by exact Classical.propComplete P
                grind
            aesop
          | inr h4 =>
            have h5 : Z = {True} := by grind
            rw [h5] at h2; simp only [Set.preimage_singleton_true] at h2; rw [<- h2]; tauto
        | inr h3 => cases (Classical.em _ : False ∈ Z ∨ False ∉ Z) with
          | inl h4 =>
            have h5 : Z = {False} := by grind
            rw [h5] at h2
            simp only [Set.preimage_singleton_false]
              at h2
            rw [<- h2]; apply MeasurableSet.compl
            tauto
          | inr h4 =>
            have : Z = ∅ := by
              ext P; constructor
              · intro h5
                have : P = True ∨ P = False
                := by exact Classical.propComplete P
                grind
              · simp
            aesop
  · apply MeasurableSpace.generateFrom_mono; intro Y h; apply Set.mem_setOf.2
    apply Set.mem_setOf.1 at h
    cases h with
    | intro a h2 =>
      unfold MeasurableSet; use a; rw [<- h2]; unfold Prop.instMeasurableSpace MeasurableSpace.comap
      simp only [MeasurableSpace.measurableSet_top, true_and]; tauto

lemma countable_set_measure_support
      {A : Type u} {_ : Uncountable A} {X : Set (Set A)} (meas : MeasurableSet X) :
      ∃ Y : Set A, Set.Countable Y ∧ ∀ Z W : Set A, Z ∩ Y = W ∩ Y → (Z ∈ X ↔ W ∈ X) := by
  rw [Set_instMeasurableSpace_generatedFrom] at meas
  unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.generateFrom at meas
  simp only at meas
  induction meas with
  | basic u a =>
    apply Set.mem_setOf.1 at a
    cases a with
    | intro w h =>
      use ({w}); constructor
      · norm_num
      · intro Z W h2; constructor
        · intro h3; rw [<- h] at h3; apply Set.mem_setOf.1 at h3; rw [<- h]; apply Set.mem_setOf.2
          have h3 : w ∈ W ∩ {w} := by grind
          grind
        · intro h3; rw [<- h] at h3; apply Set.mem_setOf.1 at h3; rw [<- h]; apply Set.mem_setOf.2
          have h4 : w ∈ Z ∩ {w} := by simp_all only [Set.mem_inter_iff, Set.mem_singleton_iff,
                                                     and_self]
          grind
  | empty => use ∅; constructor
             · norm_num
             · tauto
  | compl t a a' =>
    cases a' with
    | intro b h =>
      use b; constructor
      · exact h.1
      · intro Z W h2; grind
  | iUnion f a a' =>
    let g := fun n ↦ Classical.choose (a' n)
    let Y := ⋃ n, g n
    use Y; constructor
    · apply Set.countable_iUnion; intro n
      let h := Classical.choose_spec (a' n)
      tauto
    · intro Z W h
      have h2 : ∀ n, Z ∈ f n ↔ W ∈ f n := by
        intro n
        have h3 : g n ⊆ Y := by exact Set.subset_iUnion_of_subset n fun ⦃a⦄ a_1 ↦ a_1
        have h4 : Z ∩ g n = W ∩ g n := by
          have h5 : Z ∩ Y ∩ g n = Z ∩ g n := by grind
          have h6 : W ∩ Y ∩ g n = W ∩ g n := by grind
          simp_all only
        exact (Classical.choose_spec (a' n)).2 Z W h4
      simp_all only [Set.mem_iUnion]

lemma GrpCat_Uncountable : Uncountable GrpCat := by
  constructor; intro h; apply countable_iff_exists_surjective.1 at h
  cases h with
  | intro f h2 =>
    let X := Σ n : ℕ, (f n).carrier
    let Y := Set X
    let G := GrpCat.of (FreeGroup Y)
    have h3 : ∀ n, Cardinal.mk (f n).carrier < Cardinal.mk Y := by
      intro n
      have h4 : Cardinal.mk (f n).carrier ≤ Cardinal.mk X := by
        apply @Cardinal.mk_le_of_injective _ _ (Sigma.mk (n : ℕ)); apply sigma_mk_injective
      have h5 : Cardinal.mk X < Cardinal.mk (Set X) := by
        rw [@Cardinal.mk_set X]; exact Cardinal.cantor (Cardinal.mk X)
      exact Std.lt_of_le_of_lt h4 h5
    have h4 : ∀ n, Cardinal.mk (f n).carrier < Cardinal.mk G := by
      have h5 : Cardinal.mk Y ≤ Cardinal.mk G
        := @Cardinal.mk_le_of_injective _ _ .of FreeGroup.of_injective
      exact fun n ↦ Std.lt_of_lt_of_le (h3 n) h5
    have h5 : ∀ n, f n ≠ G := by grind
    unfold Function.Surjective at h2
    have h6 := h2 G
    tauto

/-!
**Theorem 8.**
* The existential quantifier on the category of groups is a non-measurable set.
* Fix a prime `p`. Let `F` be the field structure on `ℚ_[p]`. The first coordinate of the first
coordinate of the seventh coordinate of the first coordinate of the third coordinate of `F` is a
non-measurable set.
-/
theorem Exists_GrpCat_nonmeasurable : ¬MeasurableSet (@Exists GrpCat) := by
  let F := fun (Q : GrpCat → Prop) ↦ Exists Q
  let X := {P : GrpCat → Prop | F P}
  have e : (Exists : (GrpCat → Prop) → Prop) = X := rfl
  rw [e]; intro h
  let h2 := GrpCat_Uncountable
  apply countable_set_measure_support at h
  cases h with
  | intro Y h3 =>
    let h4 := h3.1
    let h5 := h3.2
    have h6 : ∃ G, G ∈ .univ \ Y := by
      by_contra h7
      have h8 : .univ ⊆ Y := by
        rw [Set.subset_def]
        simp only [Set.mem_diff, Set.mem_univ, true_and, not_exists, not_not] at h7
        simp_all only [Set.mem_univ, imp_self, implies_true]
      have h9 : Set.Countable (Set.univ : Set GrpCat)
        := by exact Set.Countable.mono h8 h4
      apply Set.not_countable_univ_iff.2 at h2; trivial
    let G := Classical.choose h6
    let h7 := h5 ∅ {G}
    have h8 : ∅ ∩ Y = {G} ∩ Y := by
      have : G ∉ Y := (Classical.choose_spec h6).2
      grind
    let h9 := h7 h8
    have h10 : ({G} : Set GrpCat) ∈ X := by tauto
    let h11 := h9.2 h10
    unfold X F at h11; apply Set.mem_setOf.1 at h11; tauto
  exact GrpCat_Uncountable

-------------------------------------------------------------------
-------------------------------------------------------------------

/-!
As is well-known, Lean, like many proof assistants, takes `1 / 0` to be `0`.
-/
theorem one_div_zero_eq_zero : 1 / 0 = 0 := rfl
/-!
Among people who work in classical mathematics, the consensus seems to be that this is the best way
to deal with division in proof assistants based on type theory, but it does lead to some issues,
such as the junk value of `riemannZeta 1`:

**Theorem 9.** `ζ(1) = (γ - log 4π)/2`, where `ζ` is the Riemann zeta function.
-/
theorem riemannZeta_one' :
    riemannZeta 1 = (Real.eulerMascheroniConstant - Complex.log (4 * Real.pi)) / 2 :=
  riemannZeta_one

theorem two_minus_three_eq_zero : 2 - 3 = 0 := rfl

/-!
**Theorem 10.** Two minus three, where subtraction is understood to be a partial function on `ℕ`, is
equal to the extended natural number `+∞`.
-/
theorem two_minus_three_eq_infty : (2).psub 3 = (⊤ : ℕ∞) := rfl

-------------------------------------------------------------------
-------------------------------------------------------------------

/-!
To keep the next theorem readable, we need to give shorthand notation for the following two
statements.

The statement of quadratic reciprocity for the Jacobi symbol.
-/
def QR := ∀ a b : ℕ, Odd a → Odd b →
  jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
/-!
The Baire category theorem (for small countably generated complete uniform spaces).
-/
def BCT := ∀ {X : Type} [inst : UniformSpace X]
  [CompleteSpace X] [(uniformity X).IsCountablyGenerated]
  {f : ℕ → Set X}, (∀ (n : ℕ), IsOpen (f n)) →
  (∀ (n : ℕ), Dense (f n)) → Dense (⋂ (n : ℕ), f n)

/-!
**Theorem 11.** Let `p` be the unique proof of quadratic reciprocity, and let `q` be the unique
proof that the Baire category theorem isn't false.
* The pair `⟨QR,p⟩` is equal to the pair `⟨¬¬BCT,q⟩`.
* `q` is a bijection.
-/
theorem unique_proofs :
    ∃ p : QR, ∃ q : ¬¬BCT, (∀ r : QR, p = r)
                         ∧ (∀ r : ¬¬BCT, q = r)
                         ∧ ⟨QR,p⟩ = (⟨¬¬BCT,q⟩ : Σ' A : Prop, A)
                         ∧ Function.Bijective q := by
  use (by unfold QR; grind [jacobiSym.quadratic_reciprocity])
  use (by apply not_not_intro; unfold BCT; intros
          apply BaireSpace.baire_property; all_goals assumption)
  repeat' constructor
  · simp only [implies_true]
  · simp only [not_not, implies_true]
  · grind
  · simp [Function.Injective]
  · simp [Function.Surjective]
/-!
Although, note that here it doesn't make sense to say that `p` is a function.
-/

namespace Theorem_12

def r : ℚ := {
  num := 1,
  den := 2,
  den_nz := by finiteness,
  reduced := by abel
}

def P : Polynomial ℕ := ⟨{
  support := {2},
  toFun :=
    fun n ↦ match n with
             | .succ (.succ 0) => 2
             | _ => 0,
  mem_support_toFun := by grind
}⟩

/-!
**Theorem 12.** The rational number `r` is equal to `1 / 2`.

The polynomial `P` is equal to the polynomial `2X^2`.

Let `A` be the result of applying the third coordinate of the
first coordinate of `P` to the natural number `2`. Let `B` be the first coordinate of `A`. For the
unique `z` in the domain of `B`, `B(z)` is equal to the third coordinate of `r`.
-/
theorem rational_polynomial_coordinates : r = 1 / 2
                                        ∧ P = Polynomial.C 2 * Polynomial.X^2
                                        ∧ let A := P.1.3 2;
                                          let B := A.1
                                          ∃ z, (∀ w, z = w)
                                              ∧ B z = r.3 := by
  repeat' constructor
  · apply Rat.ext; all_goals aesop
  · unfold Polynomial.X; rw [Polynomial.monomial_pow,Polynomial.C_mul_monomial]
    apply Polynomial.ext; intro n; unfold Polynomial.coeff P; aesop
  · simp only [Finsupp.mem_support_iff, ne_eq, implies_true]

#check_failure let A := (Polynomial.C 2 * Polynomial.X^2).1.3 2;
               let B := A.1
               ∃ z, (∀ w, z = w)
                  ∧ B z = (1 / 2 : ℚ).3

end Theorem_12

namespace Theorem_13

/-!
We have one last bit of equality-based junk. First we need to define the quotient of quadratic
reciprocity by the equivalence relation of equality.
-/
instance QR_setoid : Setoid QR where
  r := (· = ·)
  iseqv := by constructor; all_goals simp

def QR_mod_eq := Quotient QR_setoid
/-!
Now let `r` be the equivalence class of the unique proof of quadratic reciprocity under equality.
-/
def r : QR_mod_eq :=
  Quot.mk (· = ·) (by unfold QR; grind [jacobiSym.quadratic_reciprocity])
/-!
Use the axiom of choice to pick an element `q` of `QR/=`. (Choice needs us to give it `r` so that
it knows the the type `QR/=` is nonempty.)
-/
def q : QR_mod_eq := Classical.choice ⟨r⟩
/-!
`QR/=` is a singleton, since it's the quotient of a singleton, so we have that `q = r`.
-/
lemma q_eq_r : q = r := by simp
/-!
Consider the function from `QR` to `ℕ` that always takes on the value `1`. This clearly respects
the equivalence relation of equality, so it lifts to a function `f` from `QR/=` to `ℕ`.
-/
def f : QR_mod_eq → ℕ := Quot.lift (fun _ ↦ 1) (by simp)
/-!
Use the fact that `q` equals `r` to prove that `f q = 1`.
-/
lemma f_q_eq_one : f q = 1 := by rw [q_eq_r]; unfold f r; simp
/-!
Recall that `Fin n` is the type of natural numbers less than `n` (i.e., `Fin n` is like the set
`{0,1,...,n-1}`). Let `a` be `0` in the type `Fin (f q)`, `b` be `0` in the type `Fin (f r)`, and
`c` be `0` in the type `Fin 1`. For `a` and `b` we need to provide proofs that `0` is less than
`f q` and `f r`, respectively. (Fortunately, Lean is smart enough to figure out that `0 < 1` on its
own for `c`.)
-/
def a : Fin (f q) := ⟨0, by rw [f_q_eq_one]; simp⟩

def b : Fin (f r) := ⟨0, by unfold f r; simp⟩

def c : Fin 1 := 0
/-!
Now, since `f q = 1` and `f r = 1`, `Fin (f q)`, `Fin (f r)`, and `Fin 1` should all be the same
type, and, moreover, `a`, `b`, and `c` should all be the same thing.

Indeed we can almost prove this:

**Theorem 13.** `a` is equal to `b`, and `b` is equal to `c`.
-/
theorem a_eq_b_eq_c : a = b ∧ b = c := by
  constructor; all_goals rfl
/-!
But now there's an issue. If we ask Lean, it will tell us that `a` and `c` don't have the same type:
-/
#check_failure a = c
/-!
This means that it doesn't even make sense to say that `a` is equal to `c`.

However, it is easy to show that `a` and `c` are heterogeneously equal, since equality is
transitive, of course:
-/
theorem a_heq_c : ⟨Fin (f q), a⟩ = (⟨Fin 1, c⟩ : Σ X, X) := by
  have h0 : ⟨Fin (f q), a⟩ = (⟨Fin (f r), b⟩ : Σ X, X) := rfl
  have h1 : ⟨Fin (f r), b⟩ = (⟨Fin 1, c⟩ : Σ X, X) := rfl
  simp [h0,h1]

end Theorem_13

namespace Theorem_14

def IntFin (k : ℕ) := { x : ℤ // 0 ≤ x ∧ x < k }

axiom Fin_eq_IntFin_2147483649 : Fin 2147483649 = IntFin 2147483649

/-!
**Theorem 14.** If we assume axiomatically that the type of natural numbers less than `2147483649`
is equal to the type of integers in the interval [0,2147483649) and moreover that we trust the Lean
compiler, then `0 = 1`.
-/
theorem overflow : 0 = 1 := by
  let h := (cast Fin_eq_IntFin_2147483649 2147483648).2
  have h2 : (cast Fin_eq_IntFin_2147483649 2147483648).1 = -2147483648 :=
    by native_decide
  rw [h2] at h
  tauto

end Theorem_14
