internlm/Lean-Github huggingface dataset:
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
⊢ r a₁ a →
    match head✝ :: tail✝ with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
intro h
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
Tactic:
rw [hys] at hays
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays✝ :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays✝) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hays :
  match head✝ :: tail✝ with
  | [] => True
  | a_1 :: tail => r a a_1.fst
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays✝ :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays✝) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hays :
  match head✝ :: tail✝ with
  | [] => True
  | a_1 :: tail => r a a_1.fst
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
Tactic:
exact trans (t:=r) h hays
Proof state after:
no goals
Theorem: KVChain.rklex_not_nil_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
xs : KVChain r β
hcontra : KVChain.rklex s xs KVChain.nil
⊢ False
Tactic:
cases xs
Proof state after:
case mk
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
hcontra : KVChain.rklex s { toList := toList✝, ascend := ascend✝ } KVChain.nil
⊢ False
Theorem: KVChain.rklex_not_nil_right
Proof state before:
case mk
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
toList✝ : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) toList✝
hcontra : KVChain.rklex s { toList := toList✝, ascend := ascend✝ } KVChain.nil
⊢ False
Tactic:
cases hcontra
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hhead : Sigma.lex (flip r) s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case head hhead =>
  cases hhead
  case fst hheadFst => exact headFst _ _ _ _ _ _ _ _ hheadFst
  case snd hheadSnd => exact headSnd _ _ _ _ _ _ _ hheadSnd
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
htail : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case tail htail =>
  have := h_ind_ys xs htail
  exact tail _ _ _ _ _ _ htail this
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hheadFst : flip r a₁ a₂
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case fst hheadFst => exact headFst _ _ _ _ _ _ _ _ hheadFst
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
b₁ : β a₂
haxs : boundLeft a₂ xs
hheadSnd : s a₂ b₁ b₂
⊢ motive (KVChain.cons a₂ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
case snd hheadSnd => exact headSnd _ _ _ _ _ _ _ hheadSnd
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ : KVChain r β
a₁ : α
b₁ : β a₁
xs : KVChain r β
haxs : boundLeft a₁ xs
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
hheadFst : flip r a₁ a₂
⊢ motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₁, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
exact headFst _ _ _ _ _ _ _ _ hheadFst
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
b₁ : β a₂
haxs : boundLeft a₂ xs
hheadSnd : s a₂ b₁ b₂
⊢ motive (KVChain.cons a₂ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₁ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
exact headSnd _ _ _ _ _ _ _ hheadSnd
Proof state after:
no goals
Theorem: KVChain.rklex.rec
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
s : (a : α) → β a → β a → Prop
motive : (xs ys : KVChain r β) → KVChain.rklex s xs ys → Prop
nil :
  ∀ (a : α) (b : β a) (xs : KVChain r β) (haxs : boundLeft a xs),
    motive KVChain.nil (KVChain.cons a b xs haxs) (_ : KVChain.rklex s KVChain.nil (KVChain.cons a b xs haxs))
headFst :
  ∀ (a₁ a₂ : α) (b₁ : β a₁) (b₂ : β a₂) (xs ys : KVChain r β) (haxs : boundLeft a₁ xs) (hays : boundLeft a₂ ys)
    (ha₂a₁ : r a₂ a₁),
    motive (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a₁ b₁ xs haxs) (KVChain.cons a₂ b₂ ys hays))
headSnd :
  ∀ (a : α) (b₁ b₂ : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys) (hb₁b₂ : s a b₁ b₂),
    motive (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)
      (_ : KVChain.rklex s (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays))
tail :
  ∀ (a : α) (b : β a) (xs ys : KVChain r β) (haxs : boundLeft a xs) (hays : boundLeft a ys)
    (htail : KVChain.rklex s xs ys),
    motive xs ys htail →
      motive (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays)
        (_ : KVChain.rklex s (KVChain.cons a b xs haxs) (KVChain.cons a b ys hays))
xs✝¹ ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r β
hays : boundLeft a₂ ys
h_ind_ys : ∀ (x : KVChain r β) (h : KVChain.rklex s x ys), motive x ys h
xs✝ xs : KVChain r β
x✝ : ∀ (h : KVChain.rklex s xs (KVChain.cons a₂ b₂ ys hays)), motive xs (KVChain.cons a₂ b₂ ys hays) h
haxs : boundLeft a₂ xs
htail : List.lex (Sigma.lex (flip r) s) xs.toList ys.toList
this : motive xs ys htail
⊢ motive (KVChain.cons a₂ b₂ xs haxs) (KVChain.cons a₂ b₂ ys hays)
    (_ :
      List.lex (Sigma.lex (flip r) s) ({ fst := a₂, snd := b₂ } :: xs.toList) ({ fst := a₂, snd := b₂ } :: ys.toList))
Tactic:
exact tail _ _ _ _ _ _ htail this
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
⊢ a = b ∨ a < b → b = c ∨ b < c → a = c ∨ a < c
Tactic:
intro hab hbc
Proof state after:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b = c ∨ b < c
⊢ a = c ∨ a < c
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b = c ∨ b < c
⊢ a = c ∨ a < c
Tactic:
cases hab
Proof state after:
case inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
h✝ : a = b
⊢ a = c ∨ a < c

case inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
h✝ : a < b
⊢ a = c ∨ a < c
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haeqb : a = b
⊢ a = c ∨ a < c
Tactic:
case inl haeqb => cases haeqb; exact hbc
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a = c ∨ a < c
Tactic:
case inr haltb =>
  apply Or.inr
  cases hbc
  case inl hbeqc => cases hbeqc; exact haltb
  case inr hbltc => exact trans haltb hbltc
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haeqb : a = b
⊢ a = c ∨ a < c
Tactic:
cases haeqb
Proof state after:
case refl
α : Type u_1
inst✝ : LawfulLT α
a c : α
hbc : a = c ∨ a < c
⊢ a = c ∨ a < c
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
case refl
α : Type u_1
inst✝ : LawfulLT α
a c : α
hbc : a = c ∨ a < c
⊢ a = c ∨ a < c
Tactic:
exact hbc
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a = c ∨ a < c
Tactic:
apply Or.inr
Proof state after:
case h
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a < c
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
case h
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a < c
Tactic:
cases hbc
Proof state after:
case h.inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
h✝ : b = c
⊢ a < c

case h.inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
h✝ : b < c
⊢ a < c
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbeqc : b = c
⊢ a < c
Tactic:
case inl hbeqc => cases hbeqc; exact haltb
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbltc : b < c
⊢ a < c
Tactic:
case inr hbltc => exact trans haltb hbltc
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbeqc : b = c
⊢ a < c
Tactic:
cases hbeqc
Proof state after:
case refl
α : Type u_1
inst✝ : LawfulLT α
a b : α
haltb : a < b
⊢ a < b
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
case refl
α : Type u_1
inst✝ : LawfulLT α
a b : α
haltb : a < b
⊢ a < b
Tactic:
exact haltb
Proof state after:
no goals
Theorem: LawfulLT.eq_or_lt_trans
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
haltb : a < b
hbltc : b < c
⊢ a < c
Tactic:
exact trans haltb hbltc
Proof state after:
no goals
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
⊢ a = b ∨ a < b → b < c → a < c
Tactic:
intro hab hbc
Proof state after:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b < c
⊢ a < c
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b < c
⊢ a < c
Tactic:
cases hab
Proof state after:
case inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b < c
h✝ : a = b
⊢ a < c

case inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b < c
h✝ : a < b
⊢ a < c
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b < c
h : a = b
⊢ a < c
Tactic:
case inl h => cases h; exact hbc
Proof state after:
no goals
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b < c
h : a < b
⊢ a < c
Tactic:
case inr h => exact trans h hbc
Proof state after:
no goals
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b < c
h : a = b
⊢ a < c
Tactic:
cases h
Proof state after:
case refl
α : Type u_1
inst✝ : LawfulLT α
a c : α
hbc : a < c
⊢ a < c
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
case refl
α : Type u_1
inst✝ : LawfulLT α
a c : α
hbc : a < c
⊢ a < c
Tactic:
exact hbc
Proof state after:
no goals
Theorem: LawfulLT.lt_of_eq_or_lt_of_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b < c
h : a < b
⊢ a < c
Tactic:
exact trans h hbc
Proof state after:
no goals
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
⊢ a < b → b = c ∨ b < c → a < c
Tactic:
intro hab hbc
Proof state after:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
hbc : b = c ∨ b < c
⊢ a < c
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
hbc : b = c ∨ b < c
⊢ a < c
Tactic:
cases hbc
Proof state after:
case inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
h✝ : b = c
⊢ a < c

case inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
h✝ : b < c
⊢ a < c
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
h : b = c
⊢ a < c
Tactic:
case inl h => cases h; exact hab
Proof state after:
no goals
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
h : b < c
⊢ a < c
Tactic:
case inr h => exact trans hab h
Proof state after:
no goals
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
h : b = c
⊢ a < c
Tactic:
cases h
Proof state after:
case refl
α : Type u_1
inst✝ : LawfulLT α
a b : α
hab : a < b
⊢ a < b
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
case refl
α : Type u_1
inst✝ : LawfulLT α
a b : α
hab : a < b
⊢ a < b
Tactic:
exact hab
Proof state after:
no goals
Theorem: LawfulLT.lt_of_lt_of_eq_or_lt
Proof state before:
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a < b
h : b < c
⊢ a < c
Tactic:
exact trans hab h
Proof state after:
no goals
Theorem: ConnectedLT.subst
Proof state before:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
⊢ a₁ ≈ a₂ → b₁ ≈ b₂ → a₁ < b₁ → a₂ < b₂
Tactic:
intro ha hb h₁
Proof state after:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₂
Theorem: ConnectedLT.subst
Proof state before:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₂
Tactic:
apply ConnectedLT.lt_of_lt_of_not_gt _ hb.left
Proof state after:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₁
Theorem: ConnectedLT.subst
Proof state before:
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₁
Tactic:
apply ConnectedLT.lt_of_not_gt_of_lt ha.right h₁
Proof state after:
no goals