Random binop math olympiad stuff

Changes

2 changed files (+50/-4)

• BinOp.lean (new)
  • @@ -0,0 +1,46 @@
    + -- https://cjquines.com/files/binaryoperations.pdf + + import Mathlib + + -- example (f : ℝ → ℝ → ℝ) (l r : ℝ) (h : ∀ x, f l x = f x r ∧ f l x = x) : l = r := by + -- have h₁ : f l r = l := by + -- specialize h l + -- grind + -- have h₂ : f l r = r := by + -- specialize h r + -- grind + -- grind + + example {α} (f : α → α → α) (l r : α) (hl : ∀ x, f l x = x) (hr : ∀ x, f x r = x) : l = r := by + have h₁ : f l r = l := by + grind + -- have h₂ : f l r = r := by + -- grind + grind + + example {α} (f : α → α → α) (h : ∀ x y z, f x z = y ∧ ∀ z' ≠ z, f x z' ≠ y) : ∃ g : α → α → α, ∀ x y, f x (g x y) = g x (f x y) ∧ f x (g x y) = y := by + sorry + + example {α} (f g : α → α → α) (i j : α) (hid : ∀ x, f i x = x ∧ f x i = x ∧ g j x = x ∧ g x j = x) (h : ∀ x y z w, f (g x y) (g z w) = g (f x z) (f y w)) : f = g := by + have h₁ (x : α) : f x j = x := by + specialize h x j j i + grind + -- have h₁ (x : α) : f x j = x ∧ f j x = x ∧ g x i = x ∧ g i x = x := by + -- constructor + -- specialize h x j j i + -- grind + -- constructor + -- specialize h j i x j + -- grind + -- constructor + -- specialize h x i i j + -- grind + -- specialize h i x j i + -- grind + have h₂ : i = j := by + specialize hid j + grind + have h₃ (x y : α) : f x y = g x y := by + specialize h x i i y + grind + grind
• lake-manifest.json
  • @@ -5,7 +5,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "25ad02e863036591086654a3035fc0b4b5354bd4", + "rev": "f127f08ce3fbcb22bb783588afb15ab765f69b61", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -25,7 +25,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -55,7 +55,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc", + "rev": "9fcd6287835e2a229875a568986b786df0a0d3c6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -75,7 +75,7 @@
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bea1ecc5f1e6d9a3ab8e9ed72963cc1060b5805e", + "rev": "1340120ec7a034c5d833a337197adfdb079ac56b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",