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

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
⊢ ∀ ⦃env₁ env₂ : SSAEnv δ⦄, equiv env₁ env₂ → ∀ ⦃env₃ : SSAEnv δ⦄, equiv env₂ env₃ → equiv env₁ env₃
Tactic:
intros _ _ H1 _ H2 name
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ : SSAEnv δ
H1 : equiv env₁✝ env₂✝
env₃✝ : SSAEnv δ
H2 : equiv env₂✝ env₃✝
name : SSAVal
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ : SSAEnv δ
H1 : equiv env₁✝ env₂✝
env₃✝ : SSAEnv δ
H2 : equiv env₂✝ env₃✝
name : SSAVal
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝
Tactic:
specialize H1 name
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ env₃✝ : SSAEnv δ
H2 : equiv env₂✝ env₃✝
name : SSAVal
H1 : ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₂✝
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ env₃✝ : SSAEnv δ
H2 : equiv env₂✝ env₃✝
name : SSAVal
H1 : ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₂✝
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝
Tactic:
specialize H2 name
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ env₃✝ : SSAEnv δ
name : SSAVal
H1 : ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₂✝
H2 : ∀ (τ : MLIRType δ), get name τ env₂✝ = get name τ env₃✝
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁✝ env₂✝ env₃✝ : SSAEnv δ
name : SSAVal
H1 : ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₂✝
H2 : ∀ (τ : MLIRType δ), get name τ env₂✝ = get name τ env₃✝
⊢ ∀ (τ : MLIRType δ), get name τ env₁✝ = get name τ env₃✝
Tactic:
simp [H1, H2]
State after:
no goals