Theorem: LO.FirstOrder.Structure.Eq.models_eqAxiom (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
⊢ ∀ ⦃f : Sentence L⦄, f ∈ 𝐄𝐐 → inst✝¹.toStruc ⊧ f
Tactic:
intro σ h
State after:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
σ : Sentence L
h : σ ∈ 𝐄𝐐
⊢ inst✝¹.toStruc ⊧ σ

State before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
σ : Sentence L
h : σ ∈ 𝐄𝐐
⊢ inst✝¹.toStruc ⊧ σ
Tactic:
cases h <;> simp [models_def, Semiformula.vecEq, Semiterm.val_func]
State after:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
        func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

case relExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r✝ : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r✝ Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r✝ Semiterm.varSumInR)

State before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInR)
Tactic:
case relExt r =>
  simp [Semiformula.eval_rel]; intro e h; simp [congr_arg (rel r) (funext h)]
State after:
no goals

State before:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
        func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
intro e h
State after:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
    func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

State before:
case funcExt
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) =
    func f✝ fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
congr
State after:
case funcExt.e_a
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) = fun i =>
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

State before:
case funcExt.e_a
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) = fun i =>
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
funext i
State after:
case funcExt.e_a.h
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
i : Fin k✝
⊢ Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

State before:
case funcExt.e_a.h
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
f✝ : L.Func k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
i : Fin k✝
⊢ Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
exact h i
State after:
no goals

State before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInL) →
        (Semiformula.Eval inst✝¹ e Empty.elim) (Semiformula.rel r Semiterm.varSumInR)
Tactic:
simp [Semiformula.eval_rel]
State after:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
        rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

State before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
⊢ ∀ (e : Fin (k✝ + k✝) → M),
    (∀ (i : Fin k✝),
        Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) =
          Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)) →
      (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
        rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
intro e h
State after:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
    rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)

State before:
L : Language
μ : Type u_1
inst✝³ : Semiformula.Operator.Eq L
M : Type u
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : Structure.Eq L M
k✝ : ℕ
r : L.Rel k✝
e : Fin (k✝ + k✝) → M
h :
  ∀ (i : Fin k✝),
    Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i) = Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
⊢ (rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInL i)) →
    rel r fun i => Semiterm.val inst✝¹ e Empty.elim (Semiterm.varSumInR i)
Tactic:
simp [congr_arg (rel r) (funext h)]
State after:
no goals