Theorem: LeanSAT.Model.PropForm.subst_congr (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
⊢ ∀ (σ : ν₁ → PropForm ν₂), ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧
Tactic:
intro σ
State after:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧

State before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧
Tactic:
apply PropFun.ext
State after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ∀ (τ : PropAssignment ν₂), τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧

State before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ∀ (τ : PropAssignment ν₂), τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Tactic:
intro τ
State after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧

State before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Tactic:
rw [Quotient.eq] at hφ
State after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : φ₁ ≈ φ₂
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧

State before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : φ₁ ≈ φ₂
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Tactic:
rw [PropFun.satisfies_mk, PropFun.satisfies_mk, satisfies_subst, satisfies_subst,
    ← PropFun.satisfies_mk, ← PropFun.satisfies_mk, Quotient.sound hφ]
State after:
no goals