internlm/Lean-Github huggingface dataset:
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝¹ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs✝ ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs✝ ys✝
a : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : r a z₁
⊢ KVChain.rklex s
    (KVChain.cons a b (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
      (_ : boundLeft a (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))))
    (KVChain.cons a b (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
      (_ : boundLeft a (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))))
Tactic:
exact KVChain.rklex.tail h_ind
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝¹ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs✝ ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs✝ ys✝
a : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬r a z₁
hz₁a : r z₁ a
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
rw [cons_mergeWith_cons_flip hz₁a]
Proof state after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝¹ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs✝ ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs✝ ys✝
a : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬r a z₁
hz₁a : r z₁ a
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝¹ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs✝ ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs✝ ys✝
a : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬r a z₁
hz₁a : r z₁ a
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
rw [cons_mergeWith_cons_flip hz₁a]
Proof state after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝¹ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs✝ ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs✝ ys✝
a : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬r a z₁
hz₁a : r z₁ a
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)))
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) zs)))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝¹ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs✝ ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs✝ ys✝
a : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬r a z₁
hz₁a : r z₁ a
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b xs haxs) zs)))
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) zs)))
Tactic:
exact KVChain.rklex.tail (h_ind_zs _ _ $ KVChain.rklex.tail htail)
Proof state after:
no goals
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp (Lexcomb r s) a b
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
dsimp [Incomp] at h
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
⊢ Incomp r a b ∧ Incomp s a b
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hab := not_or.mp h.left
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
⊢ Incomp r a b ∧ Incomp s a b
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hba := not_or.mp h.right
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
⊢ Incomp r a b ∧ Incomp s a b
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have : Incomp r a b := ⟨hab.left, hba.left⟩
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
⊢ Incomp r a b ∧ Incomp s a b
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hsab : ¬ s a b :=
  λ h => absurd ⟨this, h⟩ hab.right
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
⊢ Incomp r a b ∧ Incomp s a b
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hsba : ¬ s b a :=
  λ h => absurd ⟨this.symm, h⟩ hba.right
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
hsba : ¬s b a
⊢ Incomp r a b ∧ Incomp s a b
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
hsba : ¬s b a
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
exact ⟨this, ⟨hsab, hsba⟩⟩
Proof state after:
no goals
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ Incomp (Lexcomb r s) a b
Tactic:
unfold Incomp
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
Tactic:
dsimp [Lexcomb]
Proof state after:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬(r a b ∨ Incomp r a b ∧ s a b) ∧ ¬(r b a ∨ Incomp r b a ∧ s b a)
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬(r a b ∨ Incomp r a b ∧ s a b) ∧ ¬(r b a ∨ Incomp r b a ∧ s b a)
Tactic:
apply And.intro <;> apply not_or.mpr
Proof state after:
case left
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r a b ∧ ¬(Incomp r a b ∧ s a b)

case right
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
Tactic:
case left =>
  exact ⟨h.left.left, h.right.left ∘ And.right⟩
Proof state after:
no goals
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
Tactic:
case right =>
  exact ⟨h.left.right, h.right.right ∘ And.right⟩
Proof state after:
no goals
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
Tactic:
exact ⟨h.left.left, h.right.left ∘ And.right⟩
Proof state after:
no goals
Theorem: Incomp_Lexcomb_iff
Proof state before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
Tactic:
exact ⟨h.left.right, h.right.right ∘ And.right⟩
Proof state after:
no goals
Theorem: List.relHead_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
⊢ relHead r as [] = True
Tactic:
cases as <;> rfl
Proof state after:
no goals
Theorem: List.relHead_cons_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
bs : List β
⊢ relHead r (a :: as) bs = predHead (r a) bs
Tactic:
cases bs <;> rfl
Proof state after:
no goals
Theorem: List.relHead_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
b : β
bs : List β
⊢ relHead r as (b :: bs) = predHead (fun a => r a b) as
Tactic:
cases as <;> rfl
Proof state after:
no goals
Theorem: List.relHead_of_trans
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
b : β
cs : List γ
⊢ predHead (fun a => r₁ a b) as → predHead (r₂ b) cs → relHead r as cs
Tactic:
cases as <;> cases cs <;> intros <;> try {intros; exact True.intro}
Proof state after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ relHead r (head✝¹ :: tail✝¹) (head✝ :: tail✝)
Theorem: List.relHead_of_trans
Proof state before:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ relHead r (head✝¹ :: tail✝¹) (head✝ :: tail✝)
Tactic:
dsimp [relHead]
Proof state after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ r head✝¹ head✝
Theorem: List.relHead_of_trans
Proof state before:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ r head✝¹ head✝
Tactic:
dsimp [predHead] at *
Proof state after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : r₁ head✝¹ b
a✝ : r₂ b head✝
⊢ r head✝¹ head✝
Theorem: List.relHead_of_trans
Proof state before:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : r₁ head✝¹ b
a✝ : r₂ b head✝
⊢ r head✝¹ head✝
Tactic:
exact trans ‹r₁ _ b› ‹r₂ b _›
Proof state after:
no goals
Theorem: List.relHead_of_trans
Proof state before:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝ : α
tail✝ : List α
a✝¹ : predHead (fun a => r₁ a b) (head✝ :: tail✝)
a✝ : predHead (r₂ b) []
⊢ relHead r (head✝ :: tail✝) []
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: List.relHead_eq_predHead_predHead
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ relHead r as bs = predHead (fun b => predHead (flip r b) as) bs
Tactic:
cases as <;> cases bs <;> rfl
Proof state after:
no goals
Theorem: List.forAll_map_eq
Proof state before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
as : List α
⊢ forAll p (map f as) = forAll (p ∘ f) as
Tactic:
induction as
Proof state after:
case nil
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []

case cons
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (map f tail✝) = forAll (p ∘ f) tail✝
⊢ forAll p (map f (head✝ :: tail✝)) = forAll (p ∘ f) (head✝ :: tail✝)
Theorem: List.forAll_map_eq
Proof state before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []
Tactic:
case nil => exact rfl
Proof state after:
no goals
Theorem: List.forAll_map_eq
Proof state before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ forAll p (map f (a :: as)) = forAll (p ∘ f) (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [List.forAll]
  rw [h_ind]
Proof state after:
no goals
Theorem: List.forAll_map_eq
Proof state before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []
Tactic:
exact rfl
Proof state after:
no goals
Theorem: List.forAll_map_eq
Proof state before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ forAll p (map f (a :: as)) = forAll (p ∘ f) (a :: as)
Tactic:
dsimp [List.forAll]
Proof state after:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ (p (f a) ∧ forAll p (map f as)) = (p (f a) ∧ forAll (p ∘ f) as)
Theorem: List.forAll_map_eq
Proof state before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ (p (f a) ∧ forAll p (map f as)) = (p (f a) ∧ forAll (p ∘ f) as)
Tactic:
rw [h_ind]
Proof state after:
no goals
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
as bs : List α
⊢ forAll p (as ++ bs) = (forAll p as ∧ forAll p bs)
Tactic:
induction as
Proof state after:
case nil
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)

case cons
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)
Tactic:
case nil => dsimp [forAll]; rw [true_and]
Proof state after:
no goals
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)
Tactic:
case cons _ _ h_ind => dsimp [forAll]; rw [h_ind, and_assoc]
Proof state after:
no goals
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)
Tactic:
dsimp [forAll]
Proof state after:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p bs = (True ∧ forAll p bs)
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p bs = (True ∧ forAll p bs)
Tactic:
rw [true_and]
Proof state after:
no goals
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)
Tactic:
dsimp [forAll]
Proof state after:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ (p head✝ ∧ forAll p (tail✝ ++ bs)) = ((p head✝ ∧ forAll p tail✝) ∧ forAll p bs)
Theorem: List.forAll_append
Proof state before:
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ (p head✝ ∧ forAll p (tail✝ ++ bs)) = ((p head✝ ∧ forAll p tail✝) ∧ forAll p bs)
Tactic:
rw [h_ind, and_assoc]
Proof state after:
no goals
Theorem: List.forAll_reverse
Proof state before:
α : Type u_1
p : α → Prop
as : List α
⊢ forAll p (reverse as) = forAll p as
Tactic:
induction as <;> simp
Proof state after:
case cons
α : Type u_1
p : α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (reverse tail✝) = forAll p tail✝
⊢ forAll p (reverse tail✝) ∧ forAll p [head✝] ↔ forAll p (head✝ :: tail✝)
Theorem: List.forAll_reverse
Proof state before:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ forAll p [a] ↔ forAll p (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [forAll]
  rw [h_ind, And.comm, and_true]
Proof state after:
no goals
Theorem: List.forAll_reverse
Proof state before:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ forAll p [a] ↔ forAll p (a :: as)
Tactic:
dsimp [forAll]
Proof state after:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ p a ∧ True ↔ p a ∧ forAll p as
Theorem: List.forAll_reverse
Proof state before:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ p a ∧ True ↔ p a ∧ forAll p as
Tactic:
rw [h_ind, And.comm, and_true]
Proof state after:
no goals
Theorem: List.forAll_reverseAux
Proof state before:
α : Type u_1
p : α → Prop
as bs : List α
⊢ forAll p (reverseAux as bs) = (forAll p as ∧ forAll p bs)
Tactic:
have : reverseAux as [] = reverse as := rfl
Proof state after:
α : Type u_1
p : α → Prop
as bs : List α
this : reverseAux as [] = reverse as
⊢ forAll p (reverseAux as bs) = (forAll p as ∧ forAll p bs)
Theorem: List.forAll_reverseAux
Proof state before:
α : Type u_1
p : α → Prop
as bs : List α
this : reverseAux as [] = reverse as
⊢ forAll p (reverseAux as bs) = (forAll p as ∧ forAll p bs)
Tactic:
rw [reverseAux_eq_append, forAll_append, this, forAll_reverse]
Proof state after:
no goals
Theorem: List.forAllRel_cons_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
bs : List β
⊢ List.forAllRel r (a :: as) bs = (forAll (r a) bs ∧ List.forAllRel r as bs)
Tactic:
simp [List.forAllRel, map, cons_bind, List.forAll]
Proof state after:
no goals