awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
α : Type w'
rw : (Language.sum.{u, v, w', 0} L (constantsOn α)).card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
rw₁ :
  lift.{w', max u v} L.card + lift.{max u v, w'} (constantsOn α).card =
    lift.{w', max u v} L.card + lift.{max u v, w'} #α
rw₂ rw₃ : lift.{w', max u v} L.card + lift.{max u v, w'} #α = lift.{w', max u v} L.card + lift.{max u v, w'} #α
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α

Tactic:
rw [withConstants, card_sum, card_constantsOn]

Premises used: FirstOrder.Language.withConstants, FirstOrder.Language.card_constantsOn, FirstOrder.Language.card_sum
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
α : Type w'
⊢ (L.lhomWithConstants α).Injective

Tactic:
LHom.sumInl_injective

Premises used: FirstOrder.Language.LHom.sumInl_injective, FirstOrder.Language.withConstants, FirstOrder.Language.lhomWithConstants
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
rw : LHom.comp (L' := L[[α]]) ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) LHom.sumInl = LHom.id L
rw₁ rw₂ : LHom.id L = LHom.id L
⊢ LHom.comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) (L.lhomWithConstants α) = LHom.id L

Tactic:
rw [lhomWithConstants, LHom.sumElim_comp_inl]

Premises used: FirstOrder.Language.LHom.sumElim_comp_inl, FirstOrder.Language.lhomWithConstants
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
simp :
  Eq (α := L[[α]] →ᴸ L[[α]]) (LHom.sumElim LHom.sumInl (LHom.comp LHom.sumInl (LHom.ofIsEmpty (constantsOn α) L)))
    (LHom.id L[[α]])
⊢ (L.lhomWithConstants α).comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id L[[α]]

Tactic:
simp only [LHom.comp_sumElim, lhomWithConstants, LHom.comp_id]

Premises used: FirstOrder.Language.LHom.comp_sumElim, FirstOrder.Language.LHom.comp_id, FirstOrder.Language.lhomWithConstants
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ Eq (α := L[[α]] →ᴸ L[[α]]) (LHom.sumElim LHom.sumInl (LHom.comp LHom.sumInl (LHom.ofIsEmpty (constantsOn α) L)))
    (LHom.id L[[α]])

Tactic:
_root_.trans (congr rfl (Subsingleton.elim _ _)) LHom.sumElim_inl_inr

Premises used: trans, FirstOrder.Language.LHom.sumElim_inl_inr, congr, Subsingleton.elim, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ Eq (α := L[[α]] →ᴸ L[[α]]) (LHom.sumElim LHom.sumInl (LHom.comp LHom.sumInl (LHom.ofIsEmpty (constantsOn α) L)))
    (LHom.id L[[α]])

Tactic:
exact _root_.trans (congr rfl (Subsingleton.elim _ _)) LHom.sumElim_inl_inr

Premises used: trans, FirstOrder.Language.LHom.sumElim_inl_inr, congr, Subsingleton.elim, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type w'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ funMap (L := L[[α]]) (Sum.inl f) x = funMap f x

Tactic:
(lhomWithConstants L α).map_onFunction f x

Premises used: FirstOrder.Language.LHom.map_onFunction, FirstOrder.Language.lhomWithConstants
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type w'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
R : L.Relations n
x : Fin n → M
⊢ RelMap (L := L[[α]]) (Sum.inl R) x = RelMap R x

Tactic:
(lhomWithConstants L α).map_onRelation R x

Premises used: FirstOrder.Language.LHom.map_onRelation, FirstOrder.Language.lhomWithConstants
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
α : Type w'
β : Type u_1
f : α → β
h_fun :
  ∀ (x : ℕ) (x_1 : L.Functions x),
    ((L.lhomWithConstantsMap f).comp LHom.sumInl).onFunction x_1 = (L.lhomWithConstants β).onFunction x_1
h_rel :
  ∀ (x : ℕ) (x_1 : L.Relations x),
    ((L.lhomWithConstantsMap f).comp LHom.sumInl).onRelation x_1 = (L.lhomWithConstants β).onRelation x_1
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β

Tactic:
ext
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
α : Type w'
β : Type u_1
f : α → β
x : ℕ
x_1 : L.Functions x
⊢ ((L.lhomWithConstantsMap f).comp LHom.sumInl).onFunction x_1 = (L.lhomWithConstants β).onFunction x_1

Tactic:
rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
α : Type w'
β : Type u_1
f : α → β
x : ℕ
x_1 : L.Relations x
⊢ ((L.lhomWithConstantsMap f).comp LHom.sumInl).onRelation x_1 = (L.lhomWithConstants β).onRelation x_1

Tactic:
rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
⊢ (L.lhomWithConstants M).IsExpansionOn M

Tactic:
⟨fun _ _ => rfl, fun _ _ => rfl⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
⊢ (L.lhomWithConstants α).IsExpansionOn M

Tactic:
⟨fun _ _ => rfl, fun _ _ => rfl⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
⊢ LHom.IsExpansionOn (L' := withConstants.{u, v, w} L (↑∅ : Type w))
    (LEquiv.toLHom (LEquiv.addEmptyConstants L (↑∅ : Type w))) M

Tactic:
L.withConstants_expansion _

Premises used: FirstOrder.Language.withConstants_expansion, FirstOrder.Language.lhomWithConstants, FirstOrder.Language.LHom.sumInl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
⊢ LHom.IsExpansionOn (L := withConstants.{u, v, w} L (↑∅ : Type w))
    (LEquiv.toLHom (LEquiv.symm (LEquiv.addEmptyConstants L (↑∅ : Type w)))) M

Tactic:
LHom.sumElim_isExpansionOn _ _ _

Premises used: FirstOrder.Language.LHom.sumElim_isExpansionOn, FirstOrder.Language.withConstants, FirstOrder.Language.LHom.sumElim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L'_1 : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
L' : Language
inst_2 : L'.Structure M
φ : L →ᴸ L'
inst_3 : φ.IsExpansionOn M
⊢ (LHom.addConstants α φ).IsExpansionOn M

Tactic:
LHom.sumMap_isExpansionOn _ _ M

Premises used: FirstOrder.Language.LHom.sumMap_isExpansionOn, FirstOrder.Language.withConstants, FirstOrder.Language.LHom.addConstants
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
a : α
x : Fin 0 → M
rw : Eq.{w + 1} (α := M) (funMap (L := L[[α]]) (n := 0) (Sum.inr a) default) (↑(L.con a) : M)
⊢ funMap (L := L[[α]]) (Sum.inr a) x = (↑(L.con a) : M)

Tactic:
rw [Unique.eq_default x]

Premises used: Unique.eq_default
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
a : α
x : Fin 0 → M
⊢ Eq.{w + 1} (α := M) (funMap (L := L[[α]]) (n := 0) (Sum.inr a) default) (↑(L.con a) : M)

Tactic:
(LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _

Premises used: FirstOrder.Language.LHom.sumInr, FirstOrder.Language.LHom.map_onFunction, FirstOrder.Language.constantMap, Sum.elim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
a : α
x : Fin 0 → M
⊢ Eq.{w + 1} (α := M) (funMap (L := L[[α]]) (n := 0) (Sum.inr a) default) (↑(L.con a) : M)

Tactic:
exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _

Premises used: FirstOrder.Language.LHom.sumInr, FirstOrder.Language.LHom.map_onFunction
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
a : (↑A : Type w)
⊢ (↑(L.con a) : M) = (↑a : M)

Tactic:
rfl

Premises used: FirstOrder.Language.constantMap, rfl, Sum.elim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
⊢ (LHom.constantsOnMap (Set.inclusion (s := A) (t := B) h)).IsExpansionOn M

Tactic:
constantsOnMap_isExpansionOn rfl

Premises used: FirstOrder.Language.constantsOnMap_isExpansionOn, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
⊢ (L.lhomWithConstantsMap (Set.inclusion (s := A) (t := B) h)).IsExpansionOn M

Tactic:
LHom.sumMap_isExpansionOn _ _ _

Premises used: FirstOrder.Language.LHom.sumMap_isExpansionOn, FirstOrder.Language.withConstants, FirstOrder.Language.lhomWithConstantsMap
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
refine_1 :
  ∀ {n : ℕ} (f_1 : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
    f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)
refine_2 :
  ∀ {n : ℕ} (r : (Language.withConstants.{u, v, w} L (↑A : Type w)).Relations n) (x : Fin n → M),
    RelMap r (f.toFun ∘ x) ↔ RelMap r x
⊢ M ↪[Language.withConstants.{u, v, w} L (↑A : Type w)] f.withConstants A

Tactic:
refine ⟨f.toEmbedding, ?_, ?_⟩
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
g : L.Functions n
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) (f.toFun ∘ x)

Tactic:
f.map_fun' g x

Premises used: FirstOrder.Language.Embedding.map_fun', FirstOrder.Language.Embedding.withConstants, Sum.elim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
g : L.Functions n
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) (f.toFun ∘ x)

Tactic:
exact f.map_fun' g x

Premises used: FirstOrder.Language.Embedding.map_fun'
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
x : Fin 0 → M
c : (constantsOn (↑A : Type w)).Functions 0
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin (n + 1) → M
c : (constantsOn (↑A : Type w)).Functions (n + 1)
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)

Tactic:
isEmptyElim c

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin (n + 1) → M
c : (constantsOn (↑A : Type w)).Functions (n + 1)
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)

Tactic:
exact isEmptyElim c
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
c : (constantsOn (↑A : Type w)).Functions n
refine_1 :
  ∀ (x : Fin 0 → M) (c : (constantsOn (↑A : Type w)).Functions 0),
    f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
      funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
refine_1₁ :
  ∀ (n : ℕ) (x : Fin (n + 1) → M) (c : (constantsOn (↑A : Type w)).Functions (n + 1)),
    f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
      funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)

Tactic:
cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
g : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n
x : Fin n → M
refine_1 :
  ∀ (g : L.Functions n),
    f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) x) =
      funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) (f.toFun ∘ x)
refine_1₁ :
  ∀ (c : (constantsOn (↑A : Type w)).Functions n),
    f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
      funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
⊢ f.toFun (funMap g x) = funMap g (f.toFun ∘ x)

Tactic:
cases g with
    | inl g => exact f.map_fun' g x
    | inr c =>
      cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
R : L.Relations n
⊢ RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) (f.toFun ∘ x) ↔
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) x

Tactic:
f.map_rel' R x

Premises used: Sum.elim, FirstOrder.Language.Embedding.map_rel'
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
R : L.Relations n
⊢ RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) (f.toFun ∘ x) ↔
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) x

Tactic:
exact f.map_rel' R x

Premises used: FirstOrder.Language.Embedding.map_rel'
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
r : Relations.{w, 0} (constantsOn (↑A : Type w)) n
⊢ RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) (f.toFun ∘ x) ↔
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) x

Tactic:
isEmptyElim r

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
r : Relations.{w, 0} (constantsOn (↑A : Type w)) n
⊢ RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) (f.toFun ∘ x) ↔
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) x

Tactic:
exact isEmptyElim r
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
R : (Language.withConstants.{u, v, w} L (↑A : Type w)).Relations n
x : Fin n → M
refine_2 :
  ∀ (R : L.Relations n),
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) (f.toFun ∘ x) ↔
      RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) x
refine_2₁ :
  ∀ (r : Relations.{w, 0} (constantsOn (↑A : Type w)) n),
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) (f.toFun ∘ x) ↔
      RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) x
⊢ RelMap R (f.toFun ∘ x) ↔ RelMap R x

Tactic:
cases R with
    | inl R => exact f.map_rel' R x
    | inr r => exact isEmptyElim r
-- Module: Mathlib.ModelTheory.Order
Goal:
P : (n : ℕ) → Language.order.Relations n → Prop
⊢ (∀ {n : ℕ} (R : Language.order.Relations n), P n R) ↔ P 2 orderRel.le

Tactic:
⟨fun h => h _, fun h n R =>
      match n, R with
      | 2, .le => h⟩

Premises used: _private.0.FirstOrder.Language.order.forall_relations.match_1, FirstOrder.Language.orderRel.le, Iff.intro
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
⊢ orderRel.le = orderRel.le

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
x : Language.order.Relations 0
⊢ False

Tactic:
cases x
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
⊢ IsEmpty ((n : ℕ) × Language.order.Functions n)

Tactic:
have : IsEmpty (Σ n, Language.order.Functions n) := isEmpty_sigma.2 inferInstance
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
this : IsEmpty ((n : ℕ) × Language.order.Functions n)
simp : ∀ (b : (l : ℕ) × Language.order.Relations l), b = default
⊢ ∀ (a : Language.order.Symbols), a = default

Tactic:
simp only [Symbols, Sum.forall, reduceCtorEq, Sum.inr.injEq, IsEmpty.forall_iff, true_and]

Premises used: reduceCtorEq, Sum.inr.injEq, FirstOrder.Language.Symbols, Sum.forall, true_and, IsEmpty.forall_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
this : IsEmpty ((n : ℕ) × Language.order.Functions n)
⊢ ∀ (b : (l : ℕ) × Language.order.Relations l), b = default

Tactic:
Unique.eq_default

Premises used: Unique.eq_default
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
this : IsEmpty ((n : ℕ) × Language.order.Functions n)
⊢ ∀ (b : (l : ℕ) × Language.order.Relations l), b = default

Tactic:
exact Unique.eq_default

Premises used: Unique.eq_default
-- Module: Mathlib.ModelTheory.Order
Goal:
⊢ Language.order.card = 1

Tactic:
simp [card]

Premises used: FirstOrder.Language.card
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
inst : L.IsOrdered
⊢ L.orderLHom.onRelation leSymb = leSymb

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Order
Goal:
⊢ Language.order.orderLHom = LHom.id Language.order

Tactic:
LHom.funext (Subsingleton.elim _ _) (Subsingleton.elim _ _)

Premises used: FirstOrder.Language.LHom.funext, Subsingleton.elim
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
simp :
  BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.reflexive leSymb) ∧
    BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.transitive leSymb)
⊢ ∀ ⦃φ : L.Sentence⦄, φ ∈ L.preorderTheory → BoundedFormula.IsUniversal φ

Tactic:
simp only [preorderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq]

Premises used: FirstOrder.Language.preorderTheory, forall_eq, forall_eq_or_imp, Set.mem_singleton_iff, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
⊢ BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.reflexive leSymb) ∧
    BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.transitive leSymb)

Tactic:
⟨leSymb.isUniversal_reflexive, leSymb.isUniversal_transitive⟩

Premises used: FirstOrder.Language.IsOrdered.leSymb, And.intro, FirstOrder.Language.Relations.isUniversal_reflexive, FirstOrder.Language.Relations.isUniversal_transitive
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
⊢ BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.reflexive leSymb) ∧
    BoundedFormula.IsUniversal.{u, v, 0} (L := L) (Relations.transitive leSymb)

Tactic:
exact ⟨leSymb.isUniversal_reflexive, leSymb.isUniversal_transitive⟩
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
⊢ L.partialOrderTheory.IsUniversal

Tactic:
Theory.IsUniversal.insert leSymb.isUniversal_antisymmetric

Premises used: FirstOrder.Language.partialOrderTheory, FirstOrder.Language.Theory.IsUniversal.insert, FirstOrder.Language.IsOrdered.leSymb, FirstOrder.Language.Relations.isUniversal_antisymmetric
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
⊢ L.linearOrderTheory.IsUniversal

Tactic:
Theory.IsUniversal.insert leSymb.isUniversal_total

Premises used: FirstOrder.Language.Relations.isUniversal_total, FirstOrder.Language.Theory.IsUniversal.insert, FirstOrder.Language.IsOrdered.leSymb, FirstOrder.Language.linearOrderTheory
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : M ⊨ L.linearOrderTheory
S : L.Substructure M
⊢ Theory.Model.{u, v, w'} (↥S) L.linearOrderTheory

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.dlo
⊢ M ⊨ L.linearOrderTheory

Tactic:
h.mono Set.subset_union_left

Premises used: Set.subset_union_left, FirstOrder.Language.Theory.Model.mono
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.linearOrderTheory
⊢ M ⊨ L.partialOrderTheory

Tactic:
h.mono (Set.subset_insert _ _)

Premises used: Set.subset_insert, FirstOrder.Language.Theory.Model.mono
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
h : M ⊨ L.partialOrderTheory
⊢ M ⊨ L.preorderTheory

Tactic:
h.mono (Set.subset_insert _ _)

Premises used: Set.subset_insert, FirstOrder.Language.Theory.Model.mono
-- Module: Mathlib.ModelTheory.Order
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
inst : L.IsOrdered
inst_1 : L.Structure M
inst_2 : LE M
inst_3 : Language.order.Structure M
inst_4 : Language.order.OrderedStructure M
inst_5 : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
rw : RelMap (L.orderLHom.onRelation leSymb) x ↔ x 0 ≤ x 1
rw₁ : RelMap (L := Language.order) leSymb x ↔ x 0 ≤ x 1
rw₂ rw₃ : x 0 ≤ x 1 ↔ x 0 ≤ x 1
⊢ RelMap.{u, v, w'} (L := L) leSymb x ↔ x 0 ≤ x 1

Tactic:
rw [← orderLHom_leSymb L, LHom.IsExpansionOn.map_onRelation, relMap_leSymb]

Premises used: FirstOrder.Language.orderLHom_leSymb, FirstOrder.Language.OrderedStructure.relMap_leSymb, FirstOrder.Language.LHom.IsExpansionOn.map_onRelation