internlm/Lean-Github huggingface dataset:
Theorem: List.forAllRel_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
⊢ List.forAllRel r as [] = True
Tactic:
induction as
Proof state after:
case nil
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ List.forAllRel r [] [] = True

case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : List.forAllRel r tail✝ [] = True
⊢ List.forAllRel r (head✝ :: tail✝) [] = True
Theorem: List.forAllRel_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ List.forAllRel r [] [] = True
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: List.forAllRel_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : List.forAllRel r as [] = True
⊢ List.forAllRel r (a :: as) [] = True
Tactic:
case cons a as h_ind => dsimp [List.forAllRel, forAll] at *; rw [h_ind, true_and]
Proof state after:
no goals
Theorem: List.forAllRel_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ List.forAllRel r [] [] = True
Tactic:
rfl
Proof state after:
no goals
Theorem: List.forAllRel_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : List.forAllRel r as [] = True
⊢ List.forAllRel r (a :: as) [] = True
Tactic:
dsimp [List.forAllRel, forAll] at *
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : forAll (fun a => True) as = True
⊢ (True ∧ forAll (fun a => True) as) = True
Theorem: List.forAllRel_nil_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
a : α
as : List α
h_ind : forAll (fun a => True) as = True
⊢ (True ∧ forAll (fun a => True) as) = True
Tactic:
rw [h_ind, true_and]
Proof state after:
no goals
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
b : β
bs : List β
⊢ List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
Tactic:
induction as
Proof state after:
case nil
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ List.forAllRel r [] (b :: bs) = (forAll (fun x => r x b) [] ∧ List.forAllRel r [] bs)

case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.forAllRel r tail✝ (b :: bs) = (forAll (fun x => r x b) tail✝ ∧ List.forAllRel r tail✝ bs)
⊢ List.forAllRel r (head✝ :: tail✝) (b :: bs) =
    (forAll (fun x => r x b) (head✝ :: tail✝) ∧ List.forAllRel r (head✝ :: tail✝) bs)
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ List.forAllRel r [] (b :: bs) = (forAll (fun x => r x b) [] ∧ List.forAllRel r [] bs)
Tactic:
case nil => dsimp [List.forAllRel, forAll]; rw[true_and]
Proof state after:
no goals
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ List.forAllRel r (a :: as) (b :: bs) = (forAll (fun x => r x b) (a :: as) ∧ List.forAllRel r (a :: as) bs)
Tactic:
case cons a as h_ind =>
  rw [forAllRel_cons_left, h_ind]
  dsimp [forAll]
  conv =>
    lhs
    rw [←and_assoc (c:=List.forAllRel _ _ _), and_assoc (a:=r a b), And.comm (a:=List.forAll _ _) (b:=List.forAll _ _), ←and_assoc]
  simp [and_assoc]
Proof state after:
no goals
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ List.forAllRel r [] (b :: bs) = (forAll (fun x => r x b) [] ∧ List.forAllRel r [] bs)
Tactic:
dsimp [List.forAllRel, forAll]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ True = (True ∧ True)
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ True = (True ∧ True)
Tactic:
rw[true_and]
Proof state after:
no goals
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ List.forAllRel r (a :: as) (b :: bs) = (forAll (fun x => r x b) (a :: as) ∧ List.forAllRel r (a :: as) bs)
Tactic:
rw [forAllRel_cons_left, h_ind]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ (forAll (r a) (b :: bs) ∧ forAll (fun x => r x b) as ∧ List.forAllRel r as bs) =
    (forAll (fun x => r x b) (a :: as) ∧ List.forAllRel r (a :: as) bs)
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ (forAll (r a) (b :: bs) ∧ forAll (fun x => r x b) as ∧ List.forAllRel r as bs) =
    (forAll (fun x => r x b) (a :: as) ∧ List.forAllRel r (a :: as) bs)
Tactic:
dsimp [forAll]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ ((r a b ∧ forAll (r a) bs) ∧ forAll (fun x => r x b) as ∧ List.forAllRel r as bs) =
    ((r a b ∧ forAll (fun x => r x b) as) ∧ List.forAllRel r (a :: as) bs)
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ ((r a b ∧ forAll (r a) bs) ∧ forAll (fun x => r x b) as ∧ List.forAllRel r as bs) =
    ((r a b ∧ forAll (fun x => r x b) as) ∧ List.forAllRel r (a :: as) bs)
Tactic:
conv =>
  lhs
  rw [←and_assoc (c:=List.forAllRel _ _ _), and_assoc (a:=r a b), And.comm (a:=List.forAll _ _) (b:=List.forAll _ _), ←and_assoc]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ (((r a b ∧ forAll (fun x => r x b) as) ∧ forAll (r a) bs) ∧ List.forAllRel r as bs) =
    ((r a b ∧ forAll (fun x => r x b) as) ∧ List.forAllRel r (a :: as) bs)
Theorem: List.forAllRel_cons_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
a : α
as : List α
h_ind : List.forAllRel r as (b :: bs) = (forAll (fun x => r x b) as ∧ List.forAllRel r as bs)
⊢ (((r a b ∧ forAll (fun x => r x b) as) ∧ forAll (r a) bs) ∧ List.forAllRel r as bs) =
    ((r a b ∧ forAll (fun x => r x b) as) ∧ List.forAllRel r (a :: as) bs)
Tactic:
simp [and_assoc]
Proof state after:
no goals
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
⊢ (∀ (a : α) (b : β), r a b → r₁ a b) → ∀ {as : List α} {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
Tactic:
intro himp as
Proof state after:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
as : List α
⊢ ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
as : List α
⊢ ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
Tactic:
induction as <;> simp
Proof state after:
case cons
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {bs : List β}, List.forAllRel r tail✝ bs → List.forAllRel r₁ tail✝ bs
⊢ ∀ {bs : List β}, forAll (r head✝) bs → List.forAllRel r tail✝ bs → forAll (r₁ head✝) bs ∧ List.forAllRel r₁ tail✝ bs
Theorem: List.forAllRel_of_forAllRel
Proof state before:
case cons
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {bs : List β}, List.forAllRel r tail✝ bs → List.forAllRel r₁ tail✝ bs
⊢ ∀ {bs : List β}, forAll (r head✝) bs → List.forAllRel r tail✝ bs → forAll (r₁ head✝) bs ∧ List.forAllRel r₁ tail✝ bs
Tactic:
intro bs ha has
Proof state after:
case cons
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {bs : List β}, List.forAllRel r tail✝ bs → List.forAllRel r₁ tail✝ bs
bs : List β
ha : forAll (r head✝) bs
has : List.forAllRel r tail✝ bs
⊢ forAll (r₁ head✝) bs ∧ List.forAllRel r₁ tail✝ bs
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ forAll (r₁ a) bs ∧ List.forAllRel r₁ as bs
Tactic:
case cons a as h_ind =>
  constructor
  case left => exact List.forAll_of_forAll (himp a) ha
  case right => exact h_ind has
Proof state after:
no goals
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ forAll (r₁ a) bs ∧ List.forAllRel r₁ as bs
Tactic:
constructor
Proof state after:
case left
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ forAll (r₁ a) bs

case right
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ List.forAllRel r₁ as bs
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ forAll (r₁ a) bs
Tactic:
case left => exact List.forAll_of_forAll (himp a) ha
Proof state after:
no goals
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ List.forAllRel r₁ as bs
Tactic:
case right => exact h_ind has
Proof state after:
no goals
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ forAll (r₁ a) bs
Tactic:
exact List.forAll_of_forAll (himp a) ha
Proof state after:
no goals
Theorem: List.forAllRel_of_forAllRel
Proof state before:
α : Type u_1
β : Type u_2
r r₁ : α → β → Prop
himp : ∀ (a : α) (b : β), r a b → r₁ a b
a : α
as : List α
h_ind : ∀ {bs : List β}, List.forAllRel r as bs → List.forAllRel r₁ as bs
bs : List β
ha : forAll (r a) bs
has : List.forAllRel r as bs
⊢ List.forAllRel r₁ as bs
Tactic:
exact h_ind has
Proof state after:
no goals
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : 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 γ
⊢ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
Tactic:
induction as <;> simp
Proof state after:
case cons
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
head✝ : α
tail✝ : List α
tail_ih✝ : forAll (fun x => r₁ x b) tail✝ → forAll (r₂ b) cs → List.forAllRel r tail✝ cs
⊢ forAll (fun x => r₁ x b) (head✝ :: tail✝) → forAll (r₂ b) cs → forAll (r head✝) cs ∧ List.forAllRel r tail✝ cs
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ forAll (fun x => r₁ x b) (a :: as) → forAll (r₂ b) cs → forAll (r a) cs ∧ List.forAllRel r as cs
Tactic:
case cons a as h_ind =>
  dsimp [List.forAllRel, forAll]
  intro habsb hbc
  constructor
  case left =>
    exact forAll_of_forAll (λ c (h : r₂ b c) => trans habsb.left h) hbc
  case right =>
    exact h_ind habsb.right hbc
Proof state after:
no goals
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ forAll (fun x => r₁ x b) (a :: as) → forAll (r₂ b) cs → forAll (r a) cs ∧ List.forAllRel r as cs
Tactic:
dsimp [List.forAllRel, forAll]
Proof state after:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ r₁ a b ∧ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ r₁ a b ∧ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as
Tactic:
intro habsb hbc
Proof state after:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as
Tactic:
constructor
Proof state after:
case left
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs

case right
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (fun a => forAll (r a) cs) as
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs
Tactic:
case left =>
  exact forAll_of_forAll (λ c (h : r₂ b c) => trans habsb.left h) hbc
Proof state after:
no goals
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (fun a => forAll (r a) cs) as
Tactic:
case right =>
  exact h_ind habsb.right hbc
Proof state after:
no goals
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs
Tactic:
exact forAll_of_forAll (λ c (h : r₂ b c) => trans habsb.left h) hbc
Proof state after:
no goals
Theorem: List.forAllRel_of_trans_forAll_forAll
Proof state before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (fun a => forAll (r a) cs) as
Tactic:
exact h_ind habsb.right hbc
Proof state after:
no goals
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
bs : List β
cs : List γ
⊢ bs ≠ [] → List.forAllRel r₁ as bs → List.forAllRel r₂ bs cs → List.forAllRel r as cs
Tactic:
intro hbs hab hbc
Proof state after:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
bs : List β
cs : List γ
hbs : bs ≠ []
hab : List.forAllRel r₁ as bs
hbc : List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
bs : List β
cs : List γ
hbs : bs ≠ []
hab : List.forAllRel r₁ as bs
hbc : List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs
Tactic:
cases bs
Proof state after:
case nil
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs

case cons
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
head✝ : β
tail✝ : List β
hbs : head✝ :: tail✝ ≠ []
hab : List.forAllRel r₁ as (head✝ :: tail✝)
hbc : List.forAllRel r₂ (head✝ :: tail✝) cs
⊢ List.forAllRel r as cs
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs
Tactic:
case nil => exact absurd rfl hbs
Proof state after:
no goals
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : List.forAllRel r₁ as (b :: bs)
hbc : List.forAllRel r₂ (b :: bs) cs
⊢ List.forAllRel r as cs
Tactic:
case cons b bs =>
  simp at hab hbc
  exact forAllRel_of_trans_forAll_forAll hab.left hbc.left
Proof state after:
no goals
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs
Tactic:
exact absurd rfl hbs
Proof state after:
no goals
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : List.forAllRel r₁ as (b :: bs)
hbc : List.forAllRel r₂ (b :: bs) cs
⊢ List.forAllRel r as cs
Tactic:
simp at hab hbc
Proof state after:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : forAll (fun x => r₁ x b) as ∧ List.forAllRel r₁ as bs
hbc : forAll (r₂ b) cs ∧ List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs
Theorem: List.forAllRel_trans
Proof state before:
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
b : β
bs : List β
hbs : b :: bs ≠ []
hab : forAll (fun x => r₁ x b) as ∧ List.forAllRel r₁ as bs
hbc : forAll (r₂ b) cs ∧ List.forAllRel r₂ bs cs
⊢ List.forAllRel r as cs
Tactic:
exact forAllRel_of_trans_forAll_forAll hab.left hbc.left
Proof state after:
no goals
Theorem: List.forAllRel_flip
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel (flip r) bs as = List.forAllRel r as bs
Tactic:
induction as <;> simp
Proof state after:
case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
head✝ : α
tail✝ : List α
tail_ih✝ : List.forAllRel (flip r) bs tail✝ = List.forAllRel r tail✝ bs
⊢ forAll (fun x => flip r x head✝) bs ∧ List.forAllRel (flip r) bs tail✝ ↔
    forAll (r head✝) bs ∧ List.forAllRel r tail✝ bs
Theorem: List.forAllRel_flip
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
a : α
as : List α
h_ind : List.forAllRel (flip r) bs as = List.forAllRel r as bs
⊢ forAll (fun x => flip r x a) bs ∧ List.forAllRel (flip r) bs as ↔ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
case cons a as h_ind =>
  rw [h_ind]; exact and_congr Iff.rfl Iff.rfl
Proof state after:
no goals
Theorem: List.forAllRel_flip
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
a : α
as : List α
h_ind : List.forAllRel (flip r) bs as = List.forAllRel r as bs
⊢ forAll (fun x => flip r x a) bs ∧ List.forAllRel (flip r) bs as ↔ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
rw [h_ind]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
a : α
as : List α
h_ind : List.forAllRel (flip r) bs as = List.forAllRel r as bs
⊢ forAll (fun x => flip r x a) bs ∧ List.forAllRel r as bs ↔ forAll (r a) bs ∧ List.forAllRel r as bs