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

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

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

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

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 r as bs ↔ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
exact and_congr Iff.rfl Iff.rfl
State after:
no goals