Theorem: LeanSAT.Model.PropFun.substL_disj (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
⊢ substL (φ₁ ⊔ φ₂) f = substL φ₁ f ⊔ substL φ₂ f
Tactic:
have ⟨φ₁, hφ₁⟩ := φ₁.exists_rep
State after:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁✝ φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ substL (φ₁✝ ⊔ φ₂) f = substL φ₁✝ f ⊔ substL φ₂ f

State before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁✝ φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ substL (φ₁✝ ⊔ φ₂) f = substL φ₁✝ f ⊔ substL φ₂ f
Tactic:
cases hφ₁
State after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ φ₂) f = substL ⟦φ₁⟧ f ⊔ substL φ₂ f

State before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ φ₂) f = substL ⟦φ₁⟧ f ⊔ substL φ₂ f
Tactic:
have ⟨φ₂, hφ₂⟩ := φ₂.exists_rep
State after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂✝ : PropFun ν₁
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ substL (⟦φ₁⟧ ⊔ φ₂✝) f = substL ⟦φ₁⟧ f ⊔ substL φ₂✝ f

State before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂✝ : PropFun ν₁
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ substL (⟦φ₁⟧ ⊔ φ₂✝) f = substL ⟦φ₁⟧ f ⊔ substL φ₂✝ f
Tactic:
cases hφ₂
State after:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = substL ⟦φ₁⟧ f ⊔ substL ⟦φ₂⟧ f

State before:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = substL ⟦φ₁⟧ f ⊔ substL ⟦φ₂⟧ f
Tactic:
rfl
State after:
no goals