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

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
b : β
cs : List γ
⊢ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
Tactic:
induction as <;> simp
State after:
case cons
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
head✝ : α
tail✝ : List α
tail_ih✝ : forAll (fun x => r₁ x b) tail✝ → forAll (r₂ b) cs → List.forAllRel r tail✝ cs
⊢ forAll (fun x => r₁ x b) (head✝ :: tail✝) → forAll (r₂ b) cs → forAll (r head✝) cs ∧ List.forAllRel r tail✝ cs

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ forAll (fun x => r₁ x b) (a :: as) → forAll (r₂ b) cs → forAll (r a) cs ∧ List.forAllRel r as cs
Tactic:
case cons a as h_ind =>
  dsimp [List.forAllRel, forAll]
  intro habsb hbc
  constructor
  case left =>
    exact forAll_of_forAll (λ c (h : r₂ b c) => trans habsb.left h) hbc
  case right =>
    exact h_ind habsb.right hbc
State after:
no goals

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ forAll (fun x => r₁ x b) (a :: as) → forAll (r₂ b) cs → forAll (r a) cs ∧ List.forAllRel r as cs
Tactic:
dsimp [List.forAllRel, forAll]
State after:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ r₁ a b ∧ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
⊢ r₁ a b ∧ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as
Tactic:
intro habsb hbc
State after:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs ∧ forAll (fun a => forAll (r a) cs) as
Tactic:
constructor
State after:
case left
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs

case right
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (fun a => forAll (r a) cs) as

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs
Tactic:
case left =>
  exact forAll_of_forAll (λ c (h : r₂ b c) => trans habsb.left h) hbc
State after:
no goals

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (fun a => forAll (r a) cs) as
Tactic:
case right =>
  exact h_ind habsb.right hbc
State after:
no goals

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (r a) cs
Tactic:
exact forAll_of_forAll (λ c (h : r₂ b c) => trans habsb.left h) hbc
State after:
no goals

State before:
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
a : α
as : List α
h_ind : forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
habsb : r₁ a b ∧ forAll (fun x => r₁ x b) as
hbc : forAll (r₂ b) cs
⊢ forAll (fun a => forAll (r a) cs) as
Tactic:
exact h_ind habsb.right hbc
State after:
no goals