α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : (R ⇒ fun x x_1 => x ↔ x_1) (fun x => p x = true) fun x => q x = true
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
dsimp [LiftFun] at hpq
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
by_cases h : p a
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
this : q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
have : q b := by rwa [← hpq h₁]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
this : q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
simp only [filter_cons_of_pos _ h, filter_cons_of_pos _ this, forall₂_cons, h₁, true_and_iff,
  rel_filter hpq h₂]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ q b = true
rwa [← hpq h₁]
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
this : ¬q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
have : ¬q b := by rwa [← hpq h₁]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
this : ¬q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
simp only [filter_cons_of_neg _ h, filter_cons_of_neg _ this, rel_filter hpq h₂]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.148999
δ : Type ?u.149002
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ ¬q b = true
rwa [← hpq h₁]