kbuzzard

  [attribute] [5722493.000000] ✅️ applying [to_additive] ▼
    [Meta.whnf] [21.000000] ✅️ Non-easy whnf: HasProd (f ∘ Sum.inl) a 
    [Meta.whnf] [21.000000] ✅️ Non-easy whnf: HasProd (f ∘ Sum.inr) b 
    [translate_detail] [4256341.000000] ✅️ translating the value fun {α} {β} {M} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f}
            {a b} h₁ h₂ ↦
          have this :=
            Eq.mpr
              (id
                (congrArg (fun _a ↦ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) _a (𝓝 (a * b)))
                  (OrderIso.map_atTop sumEquiv)))

kbuzzard

  [attribute] [380106651.000000] ✅️ applying [to_additive] ▼
    [Meta.whnf] [21.000000] ✅️ Non-easy whnf: HasProd (f ∘ Sum.inl) a 
    [Meta.whnf] [21.000000] ✅️ Non-easy whnf: HasProd (f ∘ Sum.inr) b 
    [translate_detail] [8569142.000000] ✅️ translating the value fun {α} {β} {M} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f}
            {a b} h₁ h₂ ↦
          have this :=
            Eq.mpr
              (id
                (congrArg (fun _a ↦ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) _a (𝓝 (a * b)))
                  (OrderIso.map_atTop sumEquiv)))

kbuzzard

/-
Solution to Problem 9 (arXiv:2602.05192).

Proves `theorem nine`: existence of a polynomial map F (all 5×5 minors of
mode-unfoldings, degree ≤ 5) characterizing factorizability of blockwise
scalings of determinantal tensors from cameras.

(definition docstrings and occasional comments manually added by Kevin Buzzard,
in the process of working out exactly what was proved in this Lean file)
-/

kbuzzard

import Mathlib.Tactic

/-!

# The integers

In this file we assume all standard facts about the naturals, and then build
the integers from scratch.

The strategy is to observe that every integer can be written as `a - b`

kbuzzard

universe u

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

kbuzzard

import data.real.irrational
import tactic

open real

example : irrational (sqrt 2) :=
begin
  rintro ⟨q, hq⟩,
  have hqnum : 0 ≤ q.num,
  { rw rat.num_nonneg_iff_zero_le,

kbuzzard

-- See https://github.com/leanprover-community/mathlib4/blob/489f10454a7ae53fdc6a95d2ac237cbc20e69b36/Mathlib/Algebra/Order/Positive/Field.lean#L42-L46
-- for the actual mathlib problem, which is even slower

universe u

class Preorder (α : Type u) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := λ a b => a ≤ b ∧ ¬ b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl

kbuzzard

-- see https://github.com/leanprover-community/mathlib4/pull/1099#discussion_r1051747996
import Mathlib.Mathport.Notation -- I don't understand this file well enough to remove it, but it's only notation

set_option autoImplicit false

universe u v

instance {ι : Type u} {α : ι → Type v} [∀ i, LE (α i)] : LE (∀ i, α i) where
  le x y := ∀ i, x i ≤ y i

kbuzzard

import tactic -- a bunch of tactics
import ring_theory.noetherian -- Noetherian rings
/-

# Using ideals in Lean

Throughout, `R` is a commutative ring.

## The type of ideals of a ring

kbuzzard

import geometry.euclidean.monge_point

-- let's look at the definition of the monge point of a simplex.

/-
We don't have an explicit definition of `euler_line`, but 
`affine_span ℝ {s.circumcenter, (univ : finset (fin (n + 1))).centroid ℝ s.points}` 
seems like a reasonable definition to go in `geometry.euclidean.monge_point` 
for the Euler line of a simplex. It should then be straightforward to prove that
 this really is a line (i.e., its `direction` has `finrank` equal to 1) if the