Changes
1 changed files (+124/-388)
-
-
@@ -1,11 +1,11 @@import Mathlib structure SurBase where l : List SurBase r : List SurBase structure PseudoNumber where l : List PseudoNumber r : List PseudoNumber @[grind] def SurBase.le (x y : SurBase) := def PseudoNumber.le (x y : PseudoNumber) := (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x) termination_by sizeOf x + sizeOf y decreasing_by
-
@@ -14,71 +14,77 @@ decreasing_bycases x cases y have := List.sizeOf_lt_of_mem h grind [SurBase.mk.sizeOf_spec] grind [PseudoNumber.mk.sizeOf_spec] instance : LE PseudoNumber where le x y := x.le y @[grind] lemma pseudonumber_le {x y : PseudoNumber} : LE.le x y ↔ x.le y := by rfl @[grind] def SurBase.valid (x : SurBase) := (∀ a ∈ x.l, ∀ b ∈ x.r, ¬b.le a) ∧ (x.l.Nodup ∧ ∀ a ∈ x.l, a.valid) ∧ (x.r.Nodup ∧ ∀ b ∈ x.r, b.valid) def PseudoNumber.valid (x : PseudoNumber) := (∀ a ∈ x.l, ∀ b ∈ x.r, ¬b ≤ a) ∧ (∀ a ∈ x.l, a.valid) ∧ (∀ b ∈ x.r, b.valid) decreasing_by all_goals expose_names cases x have := List.sizeOf_lt_of_mem h grind [SurBase.mk.sizeOf_spec] grind [PseudoNumber.mk.sizeOf_spec] def Sur := { x : SurBase // x.valid } def Number := { x : PseudoNumber // x.valid } def Sur.valid (x : Sur) := by def Number.valid (x : Number) := by have := x.property unfold SurBase.valid at this unfold PseudoNumber.valid at this exact this def Sur.l (x : Sur) : List Sur := x.val.l.attach.map fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.1.2 a b⟩ def Number.l (x : Number) : List Number := x.val.l.attach.map fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.1 a b⟩ def Sur.r (x : Sur) : List Sur := x.val.r.attach.map fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.2.2 a b⟩ def Number.r (x : Number) : List Number := x.val.r.attach.map fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.2 a b⟩ lemma sur_in_l {a x : Sur} : a ∈ x.l ↔ a.val ∈ x.val.l := by simp [Sur.l] lemma number_in_l {a x : Number} : a ∈ x.l ↔ a.val ∈ x.val.l := by simp [Number.l] constructor · grind · intro h use a.val, h rfl lemma sur_in_r {b x : Sur} : b ∈ x.r ↔ b.val ∈ x.val.r := by simp [Sur.r] lemma number_in_r {b x : Number} : b ∈ x.r ↔ b.val ∈ x.val.r := by simp [Number.r] constructor · grind · intro h use b.val, h rfl noncomputable instance : SizeOf Sur where noncomputable instance : SizeOf Number where sizeOf x := sizeOf x.val @[grind] lemma sur_sizeOf {x : Sur} : sizeOf x = sizeOf x.val := by rfl lemma number_sizeOf {x : Number} : sizeOf x = sizeOf x.val := by rfl lemma list_sizeOf [SizeOf α] (l : List α) : sizeOf l = 1 + (l.map (1 + sizeOf ·)).sum := by induction l · trivial · grind [List.cons.sizeOf_spec] lemma sur_l_size {x : Sur} : sizeOf x.val.l = sizeOf x.l := by simp [Sur.l, list_sizeOf, sur_sizeOf] lemma number_l_size {x : Number} : sizeOf x.val.l = sizeOf x.l := by simp [Number.l, list_sizeOf, number_sizeOf] lemma sur_r_size {x : Sur} : sizeOf x.val.r = sizeOf x.r := by simp [Sur.r, list_sizeOf, sur_sizeOf] lemma number_r_size {x : Number} : sizeOf x.val.r = sizeOf x.r := by simp [Number.r, list_sizeOf, number_sizeOf] @[grind] lemma sur_sizeOf_spec {x : Sur} : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by lemma sur_sizeOf_spec {x : Number} : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by cases _ : x.val grind [SurBase.mk.sizeOf_spec, sur_l_size, sur_r_size] grind [PseudoNumber.mk.sizeOf_spec, number_l_size, number_r_size] @[grind] def Sur.le (x y : Sur) := def Number.le (x y : Number) := (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x) termination_by sizeOf x + sizeOf y decreasing_by
-
@@ -87,39 +93,39 @@ decreasing_byhave := List.sizeOf_lt_of_mem h grind instance : LE Sur where instance : LE Number where le x y := x.le y @[grind] lemma sur_le {x y : Sur} : LE.le x y ↔ x.le y := by rfl lemma number_le {x y : Number} : LE.le x y ↔ x.le y := by rfl lemma sur_le_eq_surbase_le {x y : Sur} : x.val.le y.val ↔ x ≤ y := by rw [sur_le, Sur.le, SurBase.le] lemma number_le_eq_pseudonumber_le {x y : Number} : x.val ≤ y.val ↔ x ≤ y := by rw [number_le, Number.le, pseudonumber_le, PseudoNumber.le] constructor · intro h constructor · intro a ha have := h.1 a.val (sur_in_l.mp ha) have := h.1 a.val (number_in_l.mp ha) contrapose this rw [not_not] at this ⊢ exact sur_le_eq_surbase_le.mpr this exact number_le_eq_pseudonumber_le.mpr this · intro b hb have := h.2 b.val (sur_in_r.mp hb) have := h.2 b.val (number_in_r.mp hb) contrapose this rw [not_not] at this ⊢ exact sur_le_eq_surbase_le.mpr this exact number_le_eq_pseudonumber_le.mpr this · intro h constructor · intro a ha have := h.1 ⟨a, x.valid.2.1.2 a ha⟩ (sur_in_l.mpr ha) have := h.1 ⟨a, x.valid.2.1 a ha⟩ (number_in_l.mpr ha) contrapose this rw [not_not] at this ⊢ exact sur_le_eq_surbase_le.mp this exact number_le_eq_pseudonumber_le.mp this · intro b hb have := h.2 ⟨b, y.valid.2.2.2 b hb⟩ (sur_in_r.mpr hb) have := h.2 ⟨b, y.valid.2.2 b hb⟩ (number_in_r.mpr hb) contrapose this rw [not_not] at this ⊢ exact sur_le_eq_surbase_le.mp this exact number_le_eq_pseudonumber_le.mp this termination_by sizeOf x + sizeOf y decreasing_by · have := List.sizeOf_lt_of_mem ha
-
@@ -127,429 +133,159 @@ decreasing_by· have := List.sizeOf_lt_of_mem hb grind · have := List.sizeOf_lt_of_mem ha simp [sur_sizeOf] simp [number_sizeOf] cases _ : x.val grind [SurBase.mk.sizeOf_spec] grind [PseudoNumber.mk.sizeOf_spec] · have := List.sizeOf_lt_of_mem hb simp [sur_sizeOf] simp [number_sizeOf] cases _ : y.val grind [SurBase.mk.sizeOf_spec] grind [PseudoNumber.mk.sizeOf_spec] lemma sur_valid (x : Sur) : ∀ a ∈ x.l, ∀ b ∈ x.r, ¬b ≤ a := by lemma number_valid (x : Number) : ∀ a ∈ x.l, ∀ b ∈ x.r, ¬b ≤ a := by intro a ha b hb by_contra h apply sur_le_eq_surbase_le.mpr at h have := x.valid.1 a.val (sur_in_l.mp ha) b.val (sur_in_r.mp hb) apply number_le_eq_pseudonumber_le.mpr at h have := x.valid.1 a.val (number_in_l.mp ha) b.val (number_in_r.mp hb) grind abbrev Sur.Zero : Sur := ⟨⟨[], []⟩, by grind⟩ abbrev Number.Zero : Number := ⟨⟨[], []⟩, by grind⟩ abbrev Sur.One : Sur := ⟨⟨[Sur.Zero.val], []⟩, by grind⟩ abbrev Number.One : Number := ⟨⟨[Number.Zero.val], []⟩, by grind⟩ abbrev Sur.NegOne : Sur := ⟨⟨[], [Sur.Zero.val]⟩, by grind⟩ abbrev Number.NegOne : Number := ⟨⟨[], [Number.Zero.val]⟩, by grind⟩ example : Sur.Zero ≤ Sur.One := by rw [← sur_le_eq_surbase_le] example : Number.Zero ≤ Number.One := by rw [← number_le_eq_pseudonumber_le] grind example : Sur.NegOne ≤ Sur.One := by rw [← sur_le_eq_surbase_le] example : Number.NegOne ≤ Number.One := by rw [← number_le_eq_pseudonumber_le] grind example : Sur.Zero ≤ Sur.Zero := by rw [← sur_le_eq_surbase_le] example : Number.Zero ≤ Number.Zero := by rw [← number_le_eq_pseudonumber_le] grind example : Sur.One ≤ Sur.One := by rw [← sur_le_eq_surbase_le] example : Number.One ≤ Number.One := by rw [← number_le_eq_pseudonumber_le] grind theorem sur_trans {x y z : Sur} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by theorem pseudonumber_trans {x y z : PseudoNumber} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by by_contra hxz rw [sur_le, Sur.le] at hxy hyz hxz rw [pseudonumber_le, PseudoNumber.le] at hxy hyz hxz simp at hxz by_cases h : ∀ a ∈ x.l, ¬z ≤ a · obtain ⟨k, hk⟩ := hxz h have := @sur_trans k x y have := @pseudonumber_trans k x y grind · simp at h obtain ⟨k, hk⟩ := h have := @sur_trans y z k have := @pseudonumber_trans y z k grind termination_by sizeOf x + sizeOf y + sizeOf z decreasing_by all_goals cases _ : x cases _ : z have := List.sizeOf_lt_of_mem hk.1 grind grind [PseudoNumber.mk.sizeOf_spec] theorem number_trans {x y z : Number} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by rw [← number_le_eq_pseudonumber_le] at hxy hyz ⊢ exact pseudonumber_trans hxy hyz theorem sur_sandwich (x : Sur) : (∀ a ∈ x.l, a ≤ x) ∧ (∀ b ∈ x.r, x ≤ b) := by theorem number_sandwich (x : Number) : (∀ a ∈ x.l, a ≤ x) ∧ (∀ b ∈ x.r, x ≤ b) := by constructor · by_contra h simp at h obtain ⟨a, ha, h⟩ := h have := sur_valid x have := number_valid x have : ∃ aa ∈ a.l, x ≤ aa := by grind obtain ⟨aa, haa, haa'⟩ := this have := sur_trans haa' <| sur_sandwich a |>.1 aa haa have := sur_sandwich a have := number_trans haa' <| number_sandwich a |>.1 aa haa have := number_sandwich a grind · by_contra h simp at h obtain ⟨b, hb, h⟩ := h have := sur_valid x have := number_valid x have : ∃ bb ∈ b.r, bb ≤ x := by grind obtain ⟨bb, hbb, hbb'⟩ := this have := sur_trans (sur_sandwich b |>.2 bb hbb) hbb' have := sur_sandwich b have := number_trans (number_sandwich b |>.2 bb hbb) hbb' have := number_sandwich b grind decreasing_by · have := List.sizeOf_lt_of_mem ha grind · have := List.sizeOf_lt_of_mem hb all_goals try have := List.sizeOf_lt_of_mem ha try have := List.sizeOf_lt_of_mem hb grind theorem sur_refl (x : Sur) : x ≤ x := by rw [sur_le, Sur.le] theorem pseudonumber_refl (x : PseudoNumber) : x ≤ x := by rw [pseudonumber_le, PseudoNumber.le] constructor · by_contra h simp at h obtain ⟨a, ha, h⟩ := h have := sur_refl a have := pseudonumber_refl a grind · by_contra h simp at h obtain ⟨b, hb, h⟩ := h have := sur_refl b have := pseudonumber_refl b grind decreasing_by · have := List.sizeOf_lt_of_mem ha grind · have := List.sizeOf_lt_of_mem hb grind all_goals try have := List.sizeOf_lt_of_mem ha try have := List.sizeOf_lt_of_mem hb cases x grind [PseudoNumber.mk.sizeOf_spec] theorem sur_antisymm {x y : Sur} (h : ¬x ≤ y) : y ≤ x := by rw [sur_le, Sur.le] at h theorem number_antisymm {x y : Number} (h : ¬x ≤ y) : y ≤ x := by rw [number_le, Number.le] at h simp at h by_cases h' : ∀ a ∈ x.l, ¬y ≤ a · obtain ⟨k, hk, hkk⟩ := h h' have := sur_sandwich y |>.2 k hk exact sur_trans this hkk have := number_sandwich y |>.2 k hk exact number_trans this hkk · simp at h' obtain ⟨k, hk, hkk⟩ := h' have := sur_sandwich x |>.1 k hk exact sur_trans hkk this have := number_sandwich x |>.1 k hk exact number_trans hkk this instance : LT Sur where instance : LT Number where lt x y := ¬y ≤ x @[grind, simp] lemma sur_lt {x y : Sur} : LT.lt x y ↔ ¬y ≤ x := by rfl lemma number_lt {x y : Number} : LT.lt x y ↔ ¬y ≤ x := by rfl theorem sur_trans' {x y z : Sur} (hxy : x ≤ y) (hyz : y < z) : x < z := by theorem number_trans' {x y z : Number} (hxy : x ≤ y) (hyz : y < z) : x < z := by contrapose hyz simp at hyz ⊢ exact sur_trans hyz hxy exact number_trans hyz hxy theorem sur_trans'' {x y z : Sur} (hxy : x < y) (hyz : y ≤ z) : x < z := by theorem number_trans'' {x y z : Number} (hxy : x < y) (hyz : y ≤ z) : x < z := by contrapose hxy simp at hxy ⊢ exact sur_trans hyz hxy -- instance : PartialOrder Sur where -- le_trans := sur_trans -- le_refl := sur_refl -- le_antisymm := sur_antisymm -- abbrev SurBase.correct (x : SurBase) := -- ∀ a ∈ x.l, ∀ b ∈ x.r, a.le b -- instance : LE SurBase where -- le := SurBase.le -- structure Sur extends SurBase where -- h : SurBase.mk l r |>.correct -- hl : ∀ x ∈ l, x.correct -- hr : ∀ x ∈ r, x.correct -- inductive Sur : SurBase → Prop where -- | zero : Sur ⟨[], []⟩ -- | step : ∀ x, ∀ a ∈ x.l, ∀ b ∈ x.r, Sur a → Sur b → a ≤ b → Sur x -- #print SurBase -- structure le (x y : SurBase) where -- blah : Prop := fun x y ↦ (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x) -- end -- h : ∀ x ∈ l, ∀ y ∈ r, --match a, b with -- | SurBase.mk xl xr _, ⟨yl, yr, _⟩ => -- (∀ a ∈ xl, ¬le ⟨yl, yr⟩ a) ∧ (∀ b ∈ yr, ¬le b ⟨xl, xr⟩)) -- structure Sur where -- l : List Sur -- r : List Sur -- h : ∀ x ∈ l, ∀ y ∈ r, @SurBase.le [show SurBase Sur by grind] x y -- import Mathlib -- structure SurBase where -- l : List SurBase -- r : List SurBase -- @[grind] -- def SurBase.le (x y : SurBase) := -- (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x) -- termination_by sizeOf x + sizeOf y -- decreasing_by -- all_goals -- expose_names -- cases x -- cases y -- have := List.sizeOf_lt_of_mem h -- grind [SurBase.mk.sizeOf_spec] -- @[grind] -- def SurBase.valid (x : SurBase) := -- (∀ a ∈ x.l, ∀ b ∈ x.r, a.le b) ∧ (x.l.Nodup ∧ ∀ a ∈ x.l, a.valid) ∧ (x.r.Nodup ∧ ∀ b ∈ x.r, b.valid) -- decreasing_by -- all_goals -- expose_names -- cases x -- have := List.sizeOf_lt_of_mem h -- grind [SurBase.mk.sizeOf_spec] -- def Sur := { x : SurBase // x.valid } -- noncomputable instance : SizeOf Sur where -- sizeOf x := sizeOf x.val -- lemma sur_sizeOf {x : Sur} : sizeOf x = sizeOf x.val := by rfl -- noncomputable instance : SizeOf (Finset Sur) where -- sizeOf f := sizeOf f.toList -- lemma finset_sur_sizeOf (f : Finset Sur) : sizeOf f = sizeOf f.toList := by rfl -- def Sur.valid (x : Sur) := by -- have := x.property -- unfold SurBase.valid at this -- exact this -- def Sur.l (x : Sur) : Finset Sur := -- @Finset.mk SurBase x.val.l x.valid.2.1.1 |>.attach.map -- ⟨fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.1.2 a b⟩, by grind [Function.Injective]⟩ -- lemma sur_in_l {a x : Sur} : a ∈ x.l ↔ a.val ∈ x.val.l := by -- simp [Sur.l] -- constructor -- · grind -- · intro h -- use a.val, h -- rfl -- example (x : Sur) : x.val.l = x.l.toList.map (·.val) := by -- simp [Sur.l] -- -- apply? -- -- example (x : Sur) : x.val.l = x.l := by -- -- simp [Sur.l, finset_sur_sizeOf, finset_sur_sizeOf] -- -- have := x.valid.2.1.1 -- -- grind -- def Sur.r (x : Sur) : Finset Sur := -- @Finset.mk SurBase x.val.r x.valid.2.2.1 |>.attach.map -- ⟨fun ⟨a, b⟩ ↦ ⟨a, x.valid.2.2.2 a b⟩, by grind [Function.Injective]⟩ -- lemma sur_in_r {a x : Sur} : a ∈ x.r ↔ a.val ∈ x.val.r := by -- simp [Sur.r] -- constructor -- · grind -- · intro h -- use a.val, h -- rfl -- lemma sur_sizeOf_spec (x : Sur) : sizeOf x = 1 + sizeOf x.l + sizeOf x.r := by -- rw [sur_sizeOf] -- cases _ : x.val -- rw [SurBase.mk.sizeOf_spec] -- sorry -- #check SurBase.mk.sizeOf_spec -- @[grind] -- def Sur.le (x y : Sur) := -- (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x) -- termination_by sizeOf x + sizeOf y -- decreasing_by -- · rename_i h -- have := List.sizeOf_lt_of_mem h -- --simp only [sur_sizeOf] -- -- rename_i h -- -- apply sur_in_l at h -- sorry -- · sorry -- -- all_goals -- -- expose_names -- -- cases x -- -- cases y -- -- have := List.sizeOf_lt_of_mem h -- -- grind [SurBase.mk.sizeOf_spec] -- instance : LE Sur where -- le x y := x.le y -- @[grind] -- lemma sur_le {x y : Sur} : LE.le x y ↔ x.le y := by rfl -- lemma sur_le_eq_surbase_le {x y : Sur} : x.val.le y.val ↔ x ≤ y := by -- rw [sur_le, Sur.le, SurBase.le] -- constructor -- · intro h -- constructor -- · intro a ha -- have := h.1 a.val (sur_in_l.mp ha) -- contrapose this -- rw [not_not] at this ⊢ -- exact sur_le_eq_surbase_le.mpr this -- · intro b hb -- have := h.2 b.val (sur_in_r.mp hb) -- contrapose this -- rw [not_not] at this ⊢ -- exact sur_le_eq_surbase_le.mpr this -- · intro h -- constructor -- · intro a ha -- have := h.1 ⟨a, x.valid.2.1.2 a ha⟩ (sur_in_l.mpr ha) -- contrapose this -- rw [not_not] at this ⊢ -- exact sur_le_eq_surbase_le.mp this -- · intro b hb -- have := h.2 ⟨b, y.valid.2.2.2 b hb⟩ (sur_in_r.mpr hb) -- contrapose this -- rw [not_not] at this ⊢ -- exact sur_le_eq_surbase_le.mp this -- termination_by sizeOf x + sizeOf y -- decreasing_by -- sorry -- lemma sur_valid (x : Sur) : ∀ a ∈ x.l, ∀ b ∈ x.r, a ≤ b := by -- intro a ha b hb -- exact sur_le_eq_surbase_le.mp <| x.valid.1 a.val (sur_in_l.mp ha) b.val (sur_in_r.mp hb) -- abbrev Sur.Zero : Sur := ⟨⟨[], []⟩, by grind⟩ -- abbrev Sur.One : Sur := ⟨⟨[Sur.Zero.val], []⟩, by grind⟩ -- abbrev Sur.NegOne : Sur := ⟨⟨[], [Sur.Zero.val]⟩, by grind⟩ -- example : Sur.Zero ≤ Sur.One := by grind -- example : Sur.NegOne ≤ Sur.One := by grind -- example : Sur.Zero ≤ Sur.Zero := by grind -- example : Sur.One ≤ Sur.One := by grind -- lemma sur_trans (x y z : Sur) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by -- by_contra hxz -- rw [sur_le, Sur.le] at hxy hyz hxz -- simp at hxz -- by_cases h : ∀ a ∈ x.l, ¬z ≤ a -- · obtain ⟨k, _⟩ := hxz h -- have := sur_trans k x y -- grind -- · simp at h -- obtain ⟨k, _⟩ := h -- have := sur_trans y z k -- grind -- termination_by sizeOf x + sizeOf y + sizeOf z -- decreasing_by -- all_goals -- sorry -- -- cases _ : x.val -- -- cases _ : z.val -- -- have := List.sizeOf_lt_of_mem hk.1 -- -- grind [SurBase.mk.sizeOf_spec] -- lemma sur_sandwich (x : Sur) : ∀ a ∈ x.val.l, a.le l -- lemma Sur.refl (x : Sur) : x ≤ x := by -- by_contra hx -- rw [sur_le, SurBase.le] at hx -- simp at hx -- by_cases h : ∀ a ∈ x.val.l, ¬x.val.le a -- · obtain ⟨k, hk⟩ := hx h -- grind -- · simp at h -- obtain ⟨k, hk⟩ := h -- grind -- -- have := x.property -- -- unfold SurBase.correct at this -- -- unfold SurBase.le -- -- grind -- -- abbrev SurBase.correct (x : SurBase) := -- -- ∀ a ∈ x.l, ∀ b ∈ x.r, a.le b -- -- instance : LE SurBase where -- -- le := SurBase.le -- -- structure Sur extends SurBase where -- -- h : SurBase.mk l r |>.correct -- -- hl : ∀ x ∈ l, x.correct -- -- hr : ∀ x ∈ r, x.correct -- -- inductive Sur : SurBase → Prop where -- -- | zero : Sur ⟨[], []⟩ -- -- | step : ∀ x, ∀ a ∈ x.l, ∀ b ∈ x.r, Sur a → Sur b → a ≤ b → Sur x -- -- #print SurBase -- -- structure le (x y : SurBase) where -- -- blah : Prop := fun x y ↦ (∀ a ∈ x.l, ¬le y a) ∧ (∀ b ∈ y.r, ¬le b x) -- -- end -- -- h : ∀ x ∈ l, ∀ y ∈ r, -- --match a, b with -- -- | SurBase.mk xl xr _, ⟨yl, yr, _⟩ => -- -- (∀ a ∈ xl, ¬le ⟨yl, yr⟩ a) ∧ (∀ b ∈ yr, ¬le b ⟨xl, xr⟩)) exact number_trans hyz hxy abbrev equiv (x y : Number) := x ≤ y ∧ y ≤ x def PseudoNumber.add (x y : PseudoNumber) : PseudoNumber := ⟨x.l.map y.add ++ y.l.map x.add, x.r.map y.add ++ y.r.map x.add⟩ termination_by sizeOf x + sizeOf y decreasing_by all_goals expose_names cases x cases y have := List.sizeOf_lt_of_mem h grind [PseudoNumber.mk.sizeOf_spec] def Number.add (x y : Number) : Number := ⟨x.val.add y.val, by rw [PseudoNumber.valid] and_intros · intro a ha b hb · intro a ha -- -- structure Sur where -- -- l : List Sur -- -- r : List Sur -- -- h : ∀ x ∈ l, ∀ y ∈ r, @SurBase.le [show SurBase Sur by grind] x y ⟩
-