awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
φ : L.Formula α
x : α → M
rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
    BoundedFormula.Realize φ x default
⊢ Formula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
have rw₂ : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
Tactic: rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
φ : L.Formula α
x : α → M
rw : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
    BoundedFormula.Realize φ x default
rw₂ :
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
    BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default)
⊢ Formula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
have rw₃ : BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default ↔
  BoundedFormula.Realize.{u_6, u_7, u_2, u_5} (M := N) φ ((⇑f : (a : M) → N) ∘ x) default
Tactic: rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ
have rw : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ N ⊨ φ
Tactic: rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
φ : L.Sentence
rw : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ N ⊨ φ
⊢ M ⊨ φ ↔ N ⊨ φ
have rw₁ : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
Tactic: rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
φ : L.Sentence
rw : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ N ⊨ φ
rw₁ : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
⊢ M ⊨ φ ↔ N ⊨ φ
have rw₂ : Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ↔
  Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
Tactic: rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪ₑ[L] N
φ : L.Sentence
rw : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ N ⊨ φ
rw₁ : Formula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default ↔ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
rw₂ :
  Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ↔
    Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
⊢ M ⊨ φ ↔ N ⊨ φ
have rw₃ : Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default ↔ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
Tactic: rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (hypothesis)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)
have h : Formula.Realize.{u_5, u_6, u_2, 0} (M := N) (Formula.graph f)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑φ : (a : M) → N)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)) ↔
  Formula.Realize.{u_5, u_6, u_1, 0} (M := M) (Formula.graph f)
    (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)
Tactic: have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (hypothesis)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h :
  Formula.Realize.{u_5, u_6, u_2, 0} (M := N) (Formula.graph f)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑φ : (a : M) → N)
        (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)) ↔
    Formula.Realize.{u_5, u_6, u_1, 0} (M := M) (Formula.graph f)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) (funMap f x) x)
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)
have h₁ : Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N) ↔
  funMap f x = funMap f x
Tactic: rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h :
  Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N) ↔
    funMap f x = funMap f x
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)
have rw : Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N)
Tactic: rw [eq_comm, h]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
φ : M ↪ₑ[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
h :
  Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N) ↔
    funMap f x = funMap f x
rw : Eq.{u_2 + 1} (α := N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N) ((φ : (a : M) → N) (funMap f x) : N)
⊢ Eq.{u_2 + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)
have rw₁ : funMap f x = funMap f x
Tactic: rw [eq_comm, h]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
A : Set M
⊢ M ↪ₑ[withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)] f.toEmbedding.withConstants A
have refine : ∀ ⦃n : ℕ⦄ (φ : (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)).Formula (Fin n)) (x : Fin n → M),
  φ.Realize (M := f.toEmbedding.withConstants A) ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
Tactic: refine ⟨f, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (hypothesis)
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
A : Set M
n : ℕ
φ : (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)).Formula (Fin n)
x : Fin n → M
⊢ φ.Realize (M := f.toEmbedding.withConstants A) ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x
have h : Eq (α := (↑A : Type u_1) ⊕ Fin n → f.toEmbedding.withConstants A)
  (Sum.elim (fun (a : (↑A : Type u_1)) ↦ (↑(L.con a) : f.toEmbedding.withConstants A)) ((⇑f : (a : M) → N) ∘ x))
  ((⇑f : (a : M) → N) ∘ Sum.elim (fun (a : (↑A : Type u_1)) ↦ (↑(L.con a) : M)) x)
Tactic: have h :
    (Sum.elim (fun a ↦ ↑(L.con a)) (⇑f ∘ x) :
      ↑A ⊕ Fin n → f.toEmbedding.withConstants A) =
    f ∘ Sum.elim (fun a ↦ ↑(L.con a)) x :=
    (Sum.comp_elim _ _ _).symm
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    φ.Realize x
have refine_1 : Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
  N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
Tactic: refine
      _root_.trans ?_
        ((realize_iff_of_model_completeTheory M N
              (((L.lhomWithConstants M).onBoundedFormula φ).subst
                  (Constants.term ∘ Sum.inr ∘ x)).alls).trans
          ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    φ.Realize x
have refine_2 : M ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) ↔
  φ.Realize x
Tactic: refine
      _root_.trans ?_
        ((realize_iff_of_model_completeTheory M N
              (((L.lhomWithConstants M).onBoundedFormula φ).subst
                  (Constants.term ∘ Sum.inr ∘ x)).alls).trans
          ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
have refine_1 : Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
  Formula.Realize (M := N) (α := Empty)
    (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    Formula.Realize (M := N) (α := Empty)
      (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
have refine_1₁ : Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
  ∀ (xs : Fin 0 → N),
    BoundedFormula.Realize (α := Empty)
      (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) default xs
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    Formula.Realize (M := N) (α := Empty)
      (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
refine_1₁ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize (α := Empty)
        (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) default xs
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
have refine_1₂ : Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
  ∀ (xs : Fin 0 → N),
    ((L.lhomWithConstants M).onBoundedFormula φ).Realize
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    Formula.Realize (M := N) (α := Empty)
      (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
refine_1₁ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize (α := Empty)
        (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) default xs
refine_1₂ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      ((L.lhomWithConstants M).onBoundedFormula φ).Realize
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
have refine_1₃ : Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
  ∀ (xs : Fin 0 → N),
    BoundedFormula.Realize φ
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    Formula.Realize (M := N) (α := Empty)
      (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
refine_1₁ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize (α := Empty)
        (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) default xs
refine_1₂ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      ((L.lhomWithConstants M).onBoundedFormula φ).Realize
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
refine_1₃ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize φ
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
have refine_1₄ : BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x)
    default ↔
  ∀ (xs : Fin 0 → N),
    BoundedFormula.Realize φ
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    Formula.Realize (M := N) (α := Empty)
      (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
refine_1₁ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize (α := Empty)
        (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) default xs
refine_1₂ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      ((L.lhomWithConstants M).onBoundedFormula φ).Realize
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
refine_1₃ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize φ
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
refine_1₄ :
  BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x)
      default ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize φ
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
have refine_1₅ : BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x)
    default ↔
  BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ
    (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) default
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]