Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁ (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
⊢ t₁ = t₂
Tactic:
have e := Tableau.equality_def.mpr ⟨e₁, (saturated_duality.mp e₁)⟩
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = t₂

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = t₂
Tactic:
calc
  t₁ = ⟨t₁.tableau, t₁.saturated, t₁.consistent⟩ := by rfl;
  _  = ⟨t₂.tableau, t₂.saturated, t₂.consistent⟩ := by simp [e];
  _  = t₂                                        := by rfl;
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = { tableau := t₁.tableau, saturated := ⋯, consistent := ⋯ }
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ { tableau := t₁.tableau, saturated := ⋯, consistent := ⋯ } =
    { tableau := t₂.tableau, saturated := ⋯, consistent := ⋯ }
Tactic:
simp [e]
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ { tableau := t₂.tableau, saturated := ⋯, consistent := ⋯ } = t₂
Tactic:
rfl
State after:
no goals