Theorem: LO.System.Equiv.le (Logic/Logic/System.lean)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ 𝓢 =ₛ 𝓣 → 𝓢 ≤ₛ 𝓣
Tactic:
simp [Equiv, Reducible]
State after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ theory 𝓢 = theory 𝓣 → theory 𝓢 ⊆ theory 𝓣

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ theory 𝓢 = theory 𝓣 → theory 𝓢 ⊆ theory 𝓣
Tactic:
intro e
State after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
e : theory 𝓢 = theory 𝓣
⊢ theory 𝓢 ⊆ theory 𝓣

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
e : theory 𝓢 = theory 𝓣
⊢ theory 𝓢 ⊆ theory 𝓣
Tactic:
rw [e]
State after:
no goals