Theorem: List.forAllRel_cons_right (Algdata/Data/List/Prop.lean)

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
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)

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ True = (True ∧ True)

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
b : β
bs : List β
⊢ True = (True ∧ True)
Tactic:
rw[true_and]
State after:
no goals

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]
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)

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]
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)

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]
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)

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]
State after:
no goals