Theorem: ftr.Trans (Pdl/Closure.lean)

State before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ s ∈ ftr f m isDec u
Tactic:
rw [ftr.iff_Nth]
State after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]

State before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : s ∈ ftr f m isDec t
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rw [ftr.iff_Nth] at s_in_ftr_t
State after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]

State before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : t ∈ ftr f m isDec u
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rw [ftr.iff_Nth] at t_in_ftr_u
State after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]

State before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
s_in_ftr_t : ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [t]
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rcases s_in_ftr_t with ⟨i, s_in⟩
State after:
case intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]

State before:
case intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
t_in_ftr_u : ∃ i, t ∈ (fun X => (List.map f X).join)^[i] [u]
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
rcases t_in_ftr_u with ⟨j, t_in⟩
State after:
case intro.intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]

State before:
case intro.intro
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ ∃ i, s ∈ (fun X => (List.map f X).join)^[i] [u]
Tactic:
use i + j
State after:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i + j] [u]

State before:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i + j] [u]
Tactic:
rw [Function.iterate_add]
State after:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ ((fun X => (List.map f X).join)^[i] ∘ (fun X => (List.map f X).join)^[j]) [u]

State before:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ ((fun X => (List.map f X).join)^[i] ∘ (fun X => (List.map f X).join)^[j]) [u]
Tactic:
simp at *
State after:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] ((fun X => (List.map f X).join)^[j] [u])

State before:
case h
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] ((fun X => (List.map f X).join)^[j] [u])
Tactic:
apply biUnion_subset f i [t] ((fun X => (X.map f).join)^[j] [u]) (by simp; aesop)
State after:
case h.a
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] [t]

State before:
case h.a
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ s ∈ (fun X => (List.map f X).join)^[i] [t]
Tactic:
assumption
State after:
no goals

State before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ [t] ⊆ (fun X => (List.map f X).join)^[j] [u]
Tactic:
simp
State after:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ t ∈ (fun X => (List.map f X).join)^[j] [u]

State before:
α : Type
s t u : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
s_in : s ∈ (fun X => (List.map f X).join)^[i] [t]
j : ℕ
t_in : t ∈ (fun X => (List.map f X).join)^[j] [u]
⊢ t ∈ (fun X => (List.map f X).join)^[j] [u]
Tactic:
aesop
State after:
no goals