Simplify binop proofs for IAP

Changes

1 changed files (+14/-26)

• BinOp.lean
  • @@ -2,37 +2,25 @@
    import Mathlib - 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 + example (f : α → α → α) l r (hl : ∀ x, f l x = x) (hr : ∀ x, f x r = x) : l = r := by + have : f l r = l := by grind grind - example {α} [Nonempty α] (f : α → α → α) (h : ∀ x y, ∃ z, f x z = y ∧ ∀ z', f x z = f x z' → z = z') : ∃ g : α → α → α, ∀ x y, f x (g x y) = y ∧ g x (f x y) = y := by + example [Nonempty α] (f : α → α → α) (h : ∀ x y, ∃ z, f x z = y ∧ ∀ z', f x z = f x z' → z = z') : ∃ g : α → α → α, ∀ x y, f x (g x y) = y ∧ g x (f x y) = y := by let g x y := (f x).invFun y use g intro x y constructor - have h₁ x : (f x).Surjective := by - intro y - specialize h x y - grind - apply Function.rightInverse_invFun (h₁ x) - have h₁ x : (f x).Injective := by - intro a b - specialize h x (f x a) - obtain ⟨a', ⟨h₂, h₃⟩⟩ := h - rw [← h₃ a h₂] - exact h₃ b - apply Function.leftInverse_invFun (h₁ x) + · have h₁ x : (f x).Surjective := by + intro y + grind [h x y] + apply Function.rightInverse_invFun (h₁ x) + · have h₁ x : (f x).Injective := by + intro a b + grind [h x (f x a)] + apply Function.leftInverse_invFun (h₁ x) - 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₂ : 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 + 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 : i = j := by grind [hid j] + have {x y} : f x y = g x y := by grind [h x i i y] grind