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

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel r (reverse as) bs = List.forAllRel r as bs
Tactic:
induction bs generalizing as <;> simp
State after:
case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)
Tactic:
case cons _ _ h_ind =>
  rw [h_ind]; intros; exact Iff.rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)
Tactic:
rw [h_ind]
State after:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝)

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝)
Tactic:
intros
State after:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
a✝ : forAll (fun x => r x head✝) as
⊢ List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
a✝ : forAll (fun x => r x head✝) as
⊢ List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝
Tactic:
exact Iff.rfl
State after:
no goals