Theorem: SSAScope.equiv_trans (MLIR/Semantics/SSAEnv.lean)

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
⊢ equiv scope₁ scope₂ → ∀ ⦃scope₃ : SSAScope δ⦄, equiv scope₂ scope₃ → equiv scope₁ scope₃
Tactic:
intros H1 scope₃ H2 name τ
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
H1 : equiv scope₁ scope₂
scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
⊢ get name scope₁ τ = get name scope₃ τ

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
H1 : equiv scope₁ scope₂
scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
⊢ get name scope₁ τ = get name scope₃ τ
Tactic:
specialize H1 name τ
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
⊢ get name scope₁ τ = get name scope₃ τ

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
⊢ get name scope₁ τ = get name scope₃ τ
Tactic:
specialize H2 name τ
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
H2 : get name scope₂ τ = get name scope₃ τ
⊢ get name scope₁ τ = get name scope₃ τ

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
H2 : get name scope₂ τ = get name scope₃ τ
⊢ get name scope₁ τ = get name scope₃ τ
Tactic:
simp [H1, H2]
State after:
no goals