Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
import Pretty.Claims.MeasRender
/--
Measure computation at higher column position or indentation level
is worse
-/
lemma MeasRender_dom_monotonic { F : Factory α }
( h : MeasRender F d c i m₁ ) ( h' : MeasRender F d c' i' m₂ )
( h_c : c ≤ c' ) ( h_i : i ≤ i' ) : dominates F m₁ m₂ := by {
induction d generalizing c c' i i' m₁ m₂ text nl concat nest align choice
case text =>
cases h
cases h'
simp only [
dominates , add_le_add_iff_right , Bool.decide_and , Bool.decide_coe ,
Bool.and_eq_true , decide_eq_true_eq
]
constructor text.text.left text.text.right
case left => linarith
case right => dwi { apply F . text_monotonic }
case nl =>
cases h
cases h'
simp only [
dominates , Bool.decide_and , Bool.decide_coe , Bool.and_eq_true ,
decide_eq_true_eq
]
dwi { constructor }
case right => dwi { apply Factory.nl_monotonic }
case nest ih | align ih =>
cases h
rename_i h : MeasRender F d✝ c c { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h
cases h' α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ → MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → dominates F m₁ m₂ = true c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h✝ : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } nest.nest dominates F { last := last✝¹ , cost := cost✝¹ , doc := Doc.nest n✝ d✝ , x := x✝¹ , y := y✝¹ }
{ last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } = true
rename_i h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h' α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ → MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → dominates F m₁ m₂ = true c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } align.align
specialize ih h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } h h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h' h_c ( α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ → MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → dominates F m₁ m₂ = true c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } align.align by α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ → MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → dominates F m₁ m₂ = true c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } simpa ) α : Type F : Factory α d✝ : Doc c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } ih : dominates F { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ }
{ last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } = true align.align
assumption
case concat ih₁ ih₂ =>
cases h
case concat h₂ h₁ h_eq =>
cases h'
case concat h₂' h₁' h_eq' =>
specialize ih₁ h₁ h₁' h_c ( by assumption )
simp only [
dominates , Bool.decide_and , Bool.decide_coe ,
Bool.and_eq_true , decide_eq_true_eq
] at ih₁
specialize ih₂ h₂ h₂' ( by simp [ ih₁ ] ) ( by assumption )
simp [ dominates ] at ih₂ ⊢
constructor
case left => simp [*]
case right =>
simp [*]
apply Factory.concat_monotonic
. simp [ ih₁ . right : ∀ {a b : Prop }, a ∧ b → b right]
. simp [ ih₂ ]
case choice => cases h
}
/--
Measure computation on a choiceless document preserves
the doc component
-/
lemma MeasRender_doc ( h_render : MeasRender F d c i m ) ( h : Choiceless d ) : m . doc = d := by {
let ⟨⟨ s , ss ⟩, h : Render d c i { fst := s , rst := ss } h ⟩ := @ Render_total d c i h
cases ss
case nil =>
let ⟨ cost , ⟨ y , h_render' ⟩⟩ := MeasRender_single_correct F h : Render d c i { fst := s , rst := [] } h
cases MeasRender_deterministic h_render h_render'
simp
case cons hd tl =>
let ⟨ cost , ⟨ y , h_render' ⟩⟩ := MeasRender_multi_correct F h : Render d c i { fst := s , rst := hd :: tl } h ( by simp )
cases MeasRender_deterministic h_render h_render'
simp
}
/--
If measure computation at higher column position or indentation level
does not exceed the computation width limit, then the current measure computation
also does not exceed the computation width limit
-/
lemma MeasRender_dom_is_good : ∀ {α : Type } {d : Doc } {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas } {F : Factory α },
MeasRender F d c i m₁ → MeasRender F d c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W MeasRender_dom_is_good { F : Factory α }
( h : MeasRender F d c i m₁ ) ( h' : MeasRender F d c' i' m₂ )
( h_c : c ≤ c' ) ( h_i : i ≤ i' ) ( h_x : m₂ . x ≤ F . W ) ( h_y : m₂ . y ≤ F . W ) :
m₁ . x ≤ F . W ∧ m₁ . y ≤ F . W := by {
induction d generalizing c c' i i' m₁ m₂ text nl concat nest align choice
case text =>
cases h
cases h' α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wtext.text
simp only [
dominates , add_le_add_iff_right , Bool.decide_and , Bool.decide_coe ,
Bool.and_eq_true , decide_eq_true_eq
] α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wtext.text
constructor α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wtext.text.left α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wtext.text.right
case left => α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wlinarith
case right =>
α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wsimp at h_y
α : Type F : Factory α s✝ : String c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .x ≤ F .Wh_y : { last := c' + String.length s✝ , cost := Factory.text F c' (String.length s✝ ) , doc := Doc.text s✝ ,
x := c' + String.length s✝ , y := i' } .y ≤ F .Wdwi { apply le_trans : ∀ {α : Type ?u.14663} [inst : Preorder α ] {a b c : α }, a ≤ b → b ≤ c → a ≤ c le_trans }
case nl =>
cases h
cases h' α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wnl.nl
simp only [
dominates , Bool.decide_and , Bool.decide_coe , Bool.and_eq_true ,
decide_eq_true_eq
] α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wnl.nl
constructor α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wnl.nl.left α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wnl.nl.right
case left =>
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wsimp at h_x h_y ⊢ α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .W
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wconstructor α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wleft α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wright
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wcase left =>
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wapply le_trans : ∀ {α : Type ?u.18588} [inst : Preorder α ] {a b c : α }, a ≤ b → b ≤ c → a ≤ c le_transα : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wb
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .W. α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wb assumption
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .W. α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa simp [ h_x ]
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wcase right =>
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wapply le_trans : ∀ {α : Type ?u.18721} [inst : Preorder α ] {a b c : α }, a ≤ b → b ≤ c → a ≤ c le_transα : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wb
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .W. α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wb assumption
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .W. α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_y : i' ≤ F .Wh_x : c' ≤ F .W ∧ i' ≤ F .Wa simp [ h_y ]
case right =>
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wsimp at h_y
α : Type F : Factory α c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' h_x : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .x ≤ F .Wh_y : { last := i' , cost := Factory.nl F i' , doc := Doc.nl , x := max c' i' , y := i' } .y ≤ F .Wdwi { apply le_trans : ∀ {α : Type ?u.19056} [inst : Preorder α ] {a b c : α }, a ≤ b → b ≤ c → a ≤ c le_trans }
case nest ih =>
cases h α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h' : MeasRender F (Doc.nest n✝ d✝ ) c' i' m₂ h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wlast✝ : ℕ cost✝ : α x✝, y✝ : ℕ h✝ : MeasRender F d✝ c (i + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } nest { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .x ≤ F .W ∧ { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .y ≤ F .W
rename_i h : MeasRender F d✝ c (i + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h' : MeasRender F (Doc.nest n✝ d✝ ) c' i' m₂ h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wlast✝ : ℕ cost✝ : α x✝, y✝ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } nest { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .x ≤ F .W ∧ { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .y ≤ F .W
cases h' α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h✝ : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .x ≤ F .Wh_y : { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .y ≤ F .Wnest.nest { last := last✝¹ , cost := cost✝¹ , doc := Doc.nest n✝ d✝ , x := x✝¹ , y := y✝¹ } .x ≤ F .W ∧ { last := last✝¹ , cost := cost✝¹ , doc := Doc.nest n✝ d✝ , x := x✝¹ , y := y✝¹ } .y ≤ F .W
rename_i h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h' α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .x ≤ F .Wh_y : { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .y ≤ F .Wnest.nest { last := last✝¹ , cost := cost✝¹ , doc := Doc.nest n✝ d✝ , x := x✝¹ , y := y✝¹ } .x ≤ F .W ∧ { last := last✝¹ , cost := cost✝¹ , doc := Doc.nest n✝ d✝ , x := x✝¹ , y := y✝¹ } .y ≤ F .W
simp at ih h_x : { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .x ≤ F .Wh_x h_y : { last := last✝ , cost := cost✝ , doc := Doc.nest n✝ d✝ , x := x✝ , y := y✝ } .y ≤ F .Wh_y ⊢ α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : y✝ ≤ F .Wnest.nest
exact ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } h h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h' h_c ( α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : y✝ ≤ F .Wnest.nest by α : Type F : Factory α n✝ : ℕ d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c (i + n✝ ) { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' (i' + n✝ ) { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : y✝ ≤ F .Wsimpa ) h_x h_y
case align ih =>
cases h α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h' : MeasRender F (Doc.align d✝ ) c' i' m₂ h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wlast✝ : ℕ cost✝ : α x✝, y✝ : ℕ h✝ : MeasRender F d✝ c c { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } align { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i y✝ } .x ≤ F .W ∧ { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i y✝ } .y ≤ F .W
rename_i h : MeasRender F d✝ c c { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h' : MeasRender F (Doc.align d✝ ) c' i' m₂ h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wlast✝ : ℕ cost✝ : α x✝, y✝ : ℕ h : MeasRender F d✝ c c { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } align { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i y✝ } .x ≤ F .W ∧ { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i y✝ } .y ≤ F .W
cases h' α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h✝ : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i' y✝ } .x ≤ F .Wh_y : { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i' y✝ } .y ≤ F .Walign.align { last := last✝¹ , cost := cost✝¹ , doc := Doc.align d✝ , x := x✝¹ , y := max i y✝¹ } .x ≤ F .W ∧ { last := last✝¹ , cost := cost✝¹ , doc := Doc.align d✝ , x := x✝¹ , y := max i y✝¹ } .y ≤ F .W
rename_i h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h' α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i' y✝ } .x ≤ F .Wh_y : { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i' y✝ } .y ≤ F .Walign.align { last := last✝¹ , cost := cost✝¹ , doc := Doc.align d✝ , x := x✝¹ , y := max i y✝¹ } .x ≤ F .W ∧ { last := last✝¹ , cost := cost✝¹ , doc := Doc.align d✝ , x := x✝¹ , y := max i y✝¹ } .y ≤ F .W
simp at ih h_x : { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i' y✝ } .x ≤ F .Wh_x h_y : { last := last✝ , cost := cost✝ , doc := Doc.align d✝ , x := x✝ , y := max i' y✝ } .y ≤ F .Wh_y ⊢ α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Walign.align x✝¹ ≤ F .W ∧ i ≤ F .W ∧ y✝¹ ≤ F .W
have := ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } h h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h' h_c ( α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Walign.align x✝¹ ≤ F .W ∧ i ≤ F .W ∧ y✝¹ ≤ F .Wby α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wsimpa ) h_x ( α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Walign.align x✝¹ ≤ F .W ∧ i ≤ F .W ∧ y✝¹ ≤ F .Wby α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .W{ last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } .y ≤ F .W{ α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .W{ last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } .y ≤ F .W
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .W{ last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } .y ≤ F .Wsimp [ h_y ]
} ) α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } .x ≤ F .W ∧ { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } .y ≤ F .Walign.align x✝¹ ≤ F .W ∧ i ≤ F .W ∧ y✝¹ ≤ F .W
simp at this α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Walign.align x✝¹ ≤ F .W ∧ i ≤ F .W ∧ y✝¹ ≤ F .W
constructor α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Walign.align.left α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Walign.align.right
case left => α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wsimp [*]
case right =>
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wconstructor α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wleft α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wright
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wcase left =>
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wapply le_trans : ∀ {α : Type ?u.32386} [inst : Preorder α ] {a b c : α }, a ≤ b → b ≤ c → a ≤ c le_transα : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wa α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wa α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wb
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .W. α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wa α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wa α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wb assumption
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .W. α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wa simp [ h_y ]
α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wcase right => α : Type F : Factory α d✝ : Doc ih : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d✝ c i m₁ →
MeasRender F d✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' last✝¹ : ℕ cost✝¹ : α x✝¹, y✝¹ : ℕ h : MeasRender F d✝ c c { last := last✝¹ , cost := cost✝¹ , doc := d✝ , x := x✝¹ , y := y✝¹ } last✝ : ℕ cost✝ : α x✝, y✝ : ℕ h' : MeasRender F d✝ c' c' { last := last✝ , cost := cost✝ , doc := d✝ , x := x✝ , y := y✝ } h_x : x✝ ≤ F .Wh_y : i' ≤ F .W ∧ y✝ ≤ F .Wthis : x✝¹ ≤ F .W ∧ y✝¹ ≤ F .Wsimp [*]
case concat ih₁ ih₂ =>
cases h
case concat h₂ h₁ h_eq =>
subst h_eq
cases h' α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂✝ : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁✝ : MeasRender F d₁✝ c' i' m₁✝ h✝ : m₂ = Meas.concat F m₁✝ m₂✝ concat
case concat h₂' h₁' h_eq' =>
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ subst h_eq'
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ simp at h_x h_y ⊢ α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .W(m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ have := MeasRender_dom_monotonic h₁ h₁' h_c h_i α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ specialize ih₁ h₁ h₁' h_c ( α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W by α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true assumption ) ( α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W by α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true simp [ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_x ] ) ( α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W by α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wthis : dominates F m₁✝¹ m₁✝ = true simp [ h_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wh_y ] ) (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ simp only [
dominates , Bool.decide_and , Bool.decide_coe ,
Bool.and_eq_true , decide_eq_true_eq
] at ih₁ : m₁✝¹ .x ≤ F .W ∧ m₁✝¹ .y ≤ F .Wih₁ (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ specialize ih₂ h₂ h₂' ( (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W by {
simp [ dominates ] at this α : Type F : Factory α d₁✝, d₂✝ : Doc ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ h_c : c ≤ c' h_i : i ≤ i' m₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_x : m₁✝ .x ≤ F .W ∧ m₂✝ .x ≤ F .Wh_y : m₁✝ .y ≤ F .W ∧ m₂✝ .y ≤ F .Wih₁ : m₁✝¹ .x ≤ F .W ∧ m₁✝¹ .y ≤ F .Wthis : m₁✝¹ .last ≤ m₁✝ .last ∧ Factory.le F m₁✝¹ .cost m₁✝ .cost = true
simp [ this ]
} ) ( (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W by assumption ) (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ simp [ dominates ] at ih₂ : m₂✝ .x ≤ F .W → m₂✝ .y ≤ F .W → m₂✝¹ .x ≤ F .W ∧ m₂✝¹ .y ≤ F .Wih₂ ⊢ (m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .W ) ∧ m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ constructor left m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .Wright m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .W
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ case left => m₁✝¹ .x ≤ F .W ∧ m₂✝¹ .x ≤ F .Wsimp [*]
α : Type F : Factory α d₁✝, d₂✝ : Doc ih₁ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₁✝ c i m₁ →
MeasRender F d₁✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W ih₂ : ∀ {c i : ℕ } {m₁ : Meas } {c' i' : ℕ } {m₂ : Meas },
MeasRender F d₂✝ c i m₁ →
MeasRender F d₂✝ c' i' m₂ → c ≤ c' → i ≤ i' → m₂ .x ≤ F .W → m₂ .y ≤ F .W → m₁ .x ≤ F .W ∧ m₁ .y ≤ F .W c, i, c', i' : ℕ m₂ : Meas h_c : c ≤ c' h_i : i ≤ i' h_x : m₂ .x ≤ F .Wh_y : m₂ .y ≤ F .Wm₁✝¹, m₂✝¹ : Meas h₂ : MeasRender F d₂✝ m₁✝¹ .last i m₂✝¹ h₁ : MeasRender F d₁✝ c i m₁✝¹ m₁✝, m₂✝ : Meas h₂' : MeasRender F d₂✝ m₁✝ .last i' m₂✝ h₁' : MeasRender F d₁✝ c' i' m₁✝ h_eq' : m₂ = Meas.concat F m₁✝ m₂✝ case right =>
m₁✝¹ .y ≤ F .W ∧ m₂✝¹ .y ≤ F .Wsimp [*]
case choice => cases h
}