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

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

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

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

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

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

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

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

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

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