Theorem: LO.Propositional.Superintuitionistic.Tableau.equality_def (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ ↔ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ → t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ → t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Tactic:
. intro h; cases h; simp;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Tactic:
. rintro ⟨h₁, h₂⟩; cases t₁; cases t₂; simp_all;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁ = t₂ → t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h : t₁ = t₂
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h : t₁ = t₂
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2
Tactic:
cases h
State after:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ : Tableau α
⊢ t₁.1 = t₁.1 ∧ t₁.2 = t₁.2

State before:
case mp.refl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ : Tableau α
⊢ t₁.1 = t₁.1 ∧ t₁.2 = t₁.2
Tactic:
simp
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
⊢ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 → t₁ = t₂
Tactic:
rintro ⟨h₁, h₂⟩
State after:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h₁ : t₁.1 = t₂.1
h₂ : t₁.2 = t₂.2
⊢ t₁ = t₂

State before:
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₁ t₂ : Tableau α
h₁ : t₁.1 = t₂.1
h₂ : t₁.2 = t₂.2
⊢ t₁ = t₂
Tactic:
cases t₁
State after:
case mpr.intro.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₂ : Tableau α
fst✝ snd✝ : Theory α
h₁ : (fst✝, snd✝).1 = t₂.1
h₂ : (fst✝, snd✝).2 = t₂.2
⊢ (fst✝, snd✝) = t₂

State before:
case mpr.intro.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
t₂ : Tableau α
fst✝ snd✝ : Theory α
h₁ : (fst✝, snd✝).1 = t₂.1
h₂ : (fst✝, snd✝).2 = t₂.2
⊢ (fst✝, snd✝) = t₂
Tactic:
cases t₂
State after:
case mpr.intro.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
fst✝¹ snd✝¹ fst✝ snd✝ : Theory α
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

State before:
case mpr.intro.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
fst✝¹ snd✝¹ fst✝ snd✝ : Theory α
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
Tactic:
simp_all
State after:
no goals