Theorem: liftedSet.fun_comp_correct (Var/liftedSet.lean)

State before:
⊢ (∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ) →
    (∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ) →
      ∀ (a : vset F α) (ρ : SPL.Config F), (f₂ ∘ f₁) (a | ρ) = (f₂' ∘ f₁') a | ρ
Tactic:
intros h₁ h₂ a ρ
State after:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ (f₂ ∘ f₁) (a | ρ) = (f₂' ∘ f₁') a | ρ

State before:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ (f₂ ∘ f₁) (a | ρ) = (f₂' ∘ f₁') a | ρ
Tactic:
simp
State after:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁ (a | ρ)) = f₂' (f₁' a) | ρ

State before:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁ (a | ρ)) = f₂' (f₁' a) | ρ
Tactic:
rw [h₁]
State after:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁' a | ρ) = f₂' (f₁' a) | ρ

State before:
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁' a | ρ) = f₂' (f₁' a) | ρ
Tactic:
rw [←h₂]
State after:
no goals