Theorem: Regex.Data.SparseSet.subset_trans (RegexCorrectness/Data/SparseSet.lean)

State before:
n : Nat
s₁ s₂ s₃ : SparseSet n
h₁ : s₁ ⊆ s₂
h₂ : s₂ ⊆ s₃
⊢ s₁ ⊆ s₃
Tactic:
intro i hi
State after:
n : Nat
s₁ s₂ s₃ : SparseSet n
h₁ : s₁ ⊆ s₂
h₂ : s₂ ⊆ s₃
i : Fin n
hi : i ∈ s₁
⊢ i ∈ s₃

State before:
n : Nat
s₁ s₂ s₃ : SparseSet n
h₁ : s₁ ⊆ s₂
h₂ : s₂ ⊆ s₃
i : Fin n
hi : i ∈ s₁
⊢ i ∈ s₃
Tactic:
exact h₂ _ (h₁ _ hi)
State after:
no goals