awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
ψ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize (φ.onBoundedFormula BoundedFormula.falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
  (φ.onBoundedFormula (equal t₁ t₂)).Realize v xs ↔ (equal t₁ t₂).Realize v xs
Tactic: induction ψ with
  | falsum => rfl
  | equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
  | rel =>
    simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
    rfl
  | imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
  | all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]
Cleared hypotheses: ψ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
ψ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize (φ.onBoundedFormula BoundedFormula.falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.equal t₁ t₂)).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v xs
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
  (φ.onBoundedFormula (rel R ts)).Realize v xs ↔ (rel R ts).Realize v xs
Tactic: induction ψ with
  | falsum => rfl
  | equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
  | rel =>
    simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
    rfl
  | imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
  | all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]
Cleared hypotheses: ψ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
ψ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize (φ.onBoundedFormula BoundedFormula.falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.equal t₁ t₂)).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.rel R ts)).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v xs
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 : ∀ {xs : Fin n → M}, (φ.onBoundedFormula f₁).Realize v xs ↔ f₁.Realize v xs)
  (ih2 : ∀ {xs : Fin n → M}, (φ.onBoundedFormula f₂).Realize v xs ↔ f₂.Realize v xs) {xs : Fin n → M},
  (φ.onBoundedFormula (f₁ ⟹ f₂)).Realize v xs ↔ (f₁ ⟹ f₂).Realize v xs
Tactic: induction ψ with
  | falsum => rfl
  | equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
  | rel =>
    simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
    rfl
  | imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
  | all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]
Cleared hypotheses: ψ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
ψ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize (φ.onBoundedFormula BoundedFormula.falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.equal t₁ t₂)).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.rel R ts)).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v xs
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : ∀ {xs : Fin n → M}, (φ.onBoundedFormula f₁).Realize v xs ↔ f₁.Realize v xs)
    (ih2 : ∀ {xs : Fin n → M}, (φ.onBoundedFormula f₂).Realize v xs ↔ f₂.Realize v xs) {xs : Fin n → M},
    (φ.onBoundedFormula (f₁ ⟹ f₂)).Realize v xs ↔ (f₁ ⟹ f₂).Realize v xs
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 : ∀ {xs : Fin (n + 1) → M}, (φ.onBoundedFormula f).Realize v xs ↔ f.Realize v xs) {xs : Fin n → M},
  (φ.onBoundedFormula (∀' f)).Realize v xs ↔ (∀' f).Realize v xs
Tactic: induction ψ with
  | falsum => rfl
  | equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
  | rel =>
    simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
    rfl
  | imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
  | all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]
Cleared hypotheses: ψ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (R.formula₁ t).Realize v ↔ RelMap R ![Term.realize v t]
have rw : (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v t]
Tactic: rw [Relations.formula₁, realize_rel, iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v t]
have refine : ∀ (x : Fin 1), Term.realize v (![t] x) = ![Term.realize v t] x
Tactic: refine congr rfl (funext fun _ => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]
have rw : (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ Term.realize v (![t₁, t₂] i)) =
  RelMap R ![Term.realize v t₁, Term.realize v t₂]
Tactic: rw [Relations.formula₂, realize_rel, iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ Term.realize v (![t₁, t₂] i)) =
    RelMap R ![Term.realize v t₁, Term.realize v t₂]
have refine_1 : Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0
Tactic: refine congr rfl (funext (Fin.cases ?_ ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
refine_1 : Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ Term.realize v (![t₁, t₂] i)) =
    RelMap R ![Term.realize v t₁, Term.realize v t₂]
have refine_2 : ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ
Tactic: refine congr rfl (funext (Fin.cases ?_ ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ (relabel g φ).Realize v ↔ φ.Realize (v ∘ g)
have rw : BoundedFormula.Realize φ (Function.comp (β := β ⊕ Fin 0) (Sum.elim v (default ∘ Fin.cast sorry)) (Sum.inl ∘ g))
    (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 0 0)) default (natAdd 0)) =
  BoundedFormula.Realize φ (v ∘ g) default
Tactic: rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw₁ : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw₂ : BoundedFormula.Realize φ (x ∘ castAdd 0) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₂ : BoundedFormula.Realize φ (x ∘ castAdd 0) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw₃ : BoundedFormula.Realize φ (x ∘ Fin.cast sorry) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₂ : BoundedFormula.Realize φ (x ∘ castAdd 0) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₃ : BoundedFormula.Realize φ (x ∘ Fin.cast ⋯) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw₄ : BoundedFormula.Realize φ (x ∘ id) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₂ : BoundedFormula.Realize φ (x ∘ castAdd 0) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₃ : BoundedFormula.Realize φ (x ∘ Fin.cast ⋯) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₄ : BoundedFormula.Realize φ (x ∘ id) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw₅ : BoundedFormula.Realize φ x (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₂ : BoundedFormula.Realize φ (x ∘ castAdd 0) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₃ : BoundedFormula.Realize φ (x ∘ Fin.cast ⋯) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₄ : BoundedFormula.Realize φ (x ∘ id) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₅ : BoundedFormula.Realize φ x (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x
have rw₆ : BoundedFormula.Realize φ x default ↔ BoundedFormula.Realize φ x default
Tactic: rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
⊢ Realize.{u, v, w, 0} (M := M) (graph f) (cons (α := fun (a : Fin (n + 1)) ↦ M) y x) ↔ funMap f x = y
have simp : (y = funMap f fun (i : Fin n) ↦ x i) ↔ funMap f x = y
Tactic: simp only [Formula.graph, Term.realize, realize_equal, Fin.cons_zero, Fin.cons_succ]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
⊢ (y = funMap f fun (i : Fin n) ↦ x i) ↔ funMap f x = y
have rw : (funMap f fun (i : Fin n) ↦ x i) = y ↔ funMap f x = y
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y ↔ φ.Realize x
have rw : BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default
Tactic: rw [Formula.Realize, iff_iff_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default
have e__xs : y = default
Tactic: congr
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ y = default
have e__xs : ∀ (i : Fin 0), y i = default i
Tactic: ext i
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : L.Formula α
⊢ Eq (α := Set (α → M)) (setOf (φ.onFormula ψ).Realize) (setOf ψ.Realize)
have h : ∀ (x : α → M),
  Membership.mem (γ := Set (α → M)) (setOf (φ.onFormula ψ).Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf ψ.Realize) x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (Realize.{u, v, w, u'} (L := L) (M := M) ((_root_.Equiv.symm equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ)
      fun (a : α) ↦ (↑(L.con a) : M)) ↔
    M ⊨ φ
have simp : BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
    ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
    ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
  M ⊨ φ
Tactic: simp only [equivSentence, _root_.Equiv.symm_symm, Equiv.coe_trans, Realize,
    BoundedFormula.realize_relabelEquiv, Function.comp]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    M ⊨ φ
have refine : BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
    ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
    ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
  BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
    ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
Tactic: refine _root_.trans ?_ BoundedFormula.realize_constantsVarsEquiv
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
have rw : BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
    ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
    ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default =
  BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
    ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
Tactic: rw [iff_iff_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default =
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
have e__v : ∀ (val : α),
  Eq.{w + 1} (α := M)
    (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
      (Sum.inl val))
    (Sum.elim (β := Empty) (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inl val))
Tactic: congr 1 with (_ | a)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
e__v :
  ∀ (val : α),
    Eq.{w + 1} (α := M)
      (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
        (Sum.inl val))
      (Sum.elim (β := Empty) (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inl val))
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default =
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
have e__v₁ : ∀ (a : Empty),
  Eq.{w + 1} (α := M)
    (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
      (Sum.inr a))
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inr a))
Tactic: congr 1 with (_ | a)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ Sentence.Realize (L := L[[α]]) M ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ) ↔
    Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
have rw : (Realize.{u, v, w, u'} (L := L) (M := M)
    ((_root_.Equiv.symm equivSentence : (a : L[[α]].Sentence) → L.Formula α)
      ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ))
    fun (a : α) ↦ (↑(L.con a) : M)) ↔
  Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
Tactic: rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
rw :
  (Realize.{u, v, w, u'} (L := L) (M := M)
      ((_root_.Equiv.symm equivSentence : (a : L[[α]].Sentence) → L.Formula α)
        ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ))
      fun (a : α) ↦ (↑(L.con a) : M)) ↔
    Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
⊢ Sentence.Realize (L := L[[α]]) M ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ) ↔
    Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
have rw₁ : (Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)) ↔
  Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
Tactic: rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
T T' : L.Theory
h : M ⊨ T
h' : M ⊨ T'
⊢ M ⊨ T ∪ T'
have simp : ∀ (h : ∀ φ ∈ T, M ⊨ φ) (h' : ∀ φ ∈ T', M ⊨ φ) (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ
Tactic: simp only [model_iff, Set.mem_union] at *
Cleared hypotheses: h, h'