awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}
S_FG : S.FG
S_in_age_N : { α := ↥S, str := inferInstance } ∈ L.age N
nonempty_S_N : Nonempty.{w + 1} (↥S ↪[L] N)
g : ↥(f.dom ⊔ LowerAdjoint.toFun (u := SetLike.coe) (closure L) {m}) ↪[L] N
g_eq : f.cod.subtype.comp f.toEquiv.toEmbedding = g.comp (Substructure.inclusion ⋯)
x : ↥(↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).dom
⊢ Eq (α := N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                        { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
                    M ≃ₚ[L] N).cod.subtype.comp
            ((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG)
                          { dom := S, cod := g.toHom.range, toEquiv := g.equivRange : M ≃ₚ[L] N } S_FG) :
                      M ≃ₚ[L] N).toEquiv.toEmbedding.comp
              (Substructure.inclusion ⋯)) :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x :
      N)
    (((↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).cod.subtype.comp
            (↑(Subtype.mk (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) f f_FG) : M ≃ₚ[L] N).toEquiv.toEmbedding :
          (a : ↥(↑⟨f, f_FG⟩ : M ≃ₚ[L] N).dom) → N)
        x :
      N)

Tactic:
simp [S, g_eq]
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
⊢ Structure.FG.{w, u, v} L ↥S

Tactic:
have S_fg : FG L S := (fg_iff_structure_fg _).1 Substructure.fg_bot
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG.{w, u, v} L ↥S
rw : { α := ↥S, str := inferInstance } ∈ L.age M
⊢ { α := ↥S, str := inferInstance } ∈ L.age N

Tactic:
rw [hN.age, ← hM.age]

Premises used: FirstOrder.Language.IsFraisseLimit.age
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG.{w, u, v} L ↥S
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
⟨S_fg, ⟨subtype _⟩⟩

Premises used: Set.Mem, FirstOrder.Language.age, setOf, Nonempty.intro, And.intro, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG.{w, u, v} L ↥S
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨S_fg, ⟨subtype _⟩⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG.{w, u, v} L ↥S
obtain :
  Structure.FG.{w, u, v} L (↑{ α := ↥S, str := inferInstance } : Type w) →
    ∀ (emb_S : ↥S ↪[L] N), Nonempty.{w + 1} (M ≃[L] N)
⊢ Nonempty.{w + 1} (M ≃[L] N)

Tactic:
obtain ⟨_, ⟨emb_S : S ↪[L] N⟩⟩ : ⟨S, inferInstance⟩ ∈ L.age N := by
    rw [hN.age, ← hM.age]
    exact ⟨S_fg, ⟨subtype _⟩⟩

Premises used: FirstOrder.Language.age
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG.{w, u, v} L ↥S
left : Structure.FG.{w, u, v} L (↑{ α := ↥S, str := inferInstance } : Type w)
emb_S : ↥S ↪[L] N
v : M ≃ₚ[L] N := { dom := S, cod := emb_S.toHom.range, toEquiv := emb_S.equivRange }
⊢ Nonempty.{w + 1} (M ≃[L] N)

Tactic:
⟨Exists.choose (equiv_between_cg cg_of_countable cg_of_countable
    ⟨v, ((Substructure.fg_iff_structure_fg _).2 S_fg)⟩ (hM.isExtensionPair hN)
      (hN.isExtensionPair hM))⟩

Premises used: Iff.mpr, FirstOrder.Language.Substructure.fg_iff_structure_fg, Nonempty.intro, Subtype.mk, FirstOrder.Language.IsFraisseLimit.isExtensionPair, FirstOrder.Language.equiv_between_cg, Exists.choose, FirstOrder.Language.Structure.cg_of_countable
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst : L.Structure M
N : Type w
inst_1 : L.Structure N
inst_2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
inst_3 : Countable M
inst_4 : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG.{w, u, v} L ↥S
left : Structure.FG.{w, u, v} L (↑{ α := ↥S, str := inferInstance } : Type w)
emb_S : ↥S ↪[L] N
v : M ≃ₚ[L] N := { dom := S, cod := emb_S.toHom.range, toEquiv := emb_S.equivRange }
⊢ Nonempty.{w + 1} (M ≃[L] N)

Tactic:
exact ⟨Exists.choose (equiv_between_cg cg_of_countable cg_of_countable
    ⟨v, ((Substructure.fg_iff_structure_fg _).2 S_fg)⟩ (hM.isExtensionPair hN)
      (hN.isExtensionPair hM))⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
⊢ Finite.{u_1 + 1} ↥S

Tactic:
have : Finite S := hS.finite
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this : Finite.{u_1 + 1} ↥S
⊢ Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }

Tactic:
have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this_1 : Finite.{u_1 + 1} ↥S
this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
⊢ Finite.{u_1 + 1} ↥f.toHom.range

Tactic:
have : Finite f.toHom.range := (((Substructure.fg_iff_structure_fg S).1 hS).range _).finite
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this_1 : Finite.{u_1 + 1} ↥S
this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
this : Finite.{u_1 + 1} ↥f.toHom.range
⊢ Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }

Tactic:
have : Infinite { x // x ∉ f.toHom.range } := ((Set.toFinite _).infinite_compl).to_subtype
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this_1 : Finite.{u_1 + 1} ↥S
this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
this_3 : Finite.{u_1 + 1} ↥f.toHom.range
this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype

Tactic:
⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩

Premises used: Nonempty.some, FirstOrder.Language.Equiv.toEquiv, FirstOrder.Language.Embedding.equivRange, Exists.intro, Equiv.subtypeCongr, nonempty_equiv_of_countable, FirstOrder.Language.StrongHomClass.toEquiv
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this_1 : Finite.{u_1 + 1} ↥S
this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
this_3 : Finite.{u_1 + 1} ↥f.toHom.range
this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }
refine :
  f =
    Embedding.comp
      (Equiv.toEmbedding
        (StrongHomClass.toEquiv
          (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range) (Nonempty.some ⋯))))
      S.subtype
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype

Tactic:
refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this_1 : Finite.{u_1 + 1} ↥S
this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
this_3 : Finite.{u_1 + 1} ↥f.toHom.range
this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }
h :
  ∀ (x : ↥S),
    Eq (α := M) ((f : (a : ↥S) → M) x : M)
      ((Embedding.comp
              (Equiv.toEmbedding
                (StrongHomClass.toEquiv
                  (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range)
                    (Nonempty.some ⋯))))
              S.subtype :
            (a : ↥S) → M)
          x :
        M)
⊢ f =
    Embedding.comp
      (Equiv.toEmbedding
        (StrongHomClass.toEquiv
          (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range) (Nonempty.some ⋯))))
      S.subtype

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this_1 : Finite.{u_1 + 1} ↥S
this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
this_3 : Finite.{u_1 + 1} ↥f.toHom.range
this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }
x : ↥S
⊢ Eq (α := M) ((f : (a : ↥S) → M) x : M)
    ((Embedding.comp
            (Equiv.toEmbedding
              (StrongHomClass.toEquiv
                (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range)
                  (Nonempty.some ⋯))))
            S.subtype :
          (a : ↥S) → M)
        x :
      M)

Tactic:
simp [Equiv.subtypeCongr]

Premises used: Equiv.subtypeCongr
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
have have₁ have₂ : ∀ (this : Finite.{u_1 + 1} ↥S), ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have₃ :
  ∀ (this : Finite.{u_1 + 1} ↥S) (this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }),
    ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have₄ :
  ∀ (this : Finite.{u_1 + 1} ↥S) (this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S })
    (this : Finite.{u_1 + 1} ↥f.toHom.range), ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have₅ :
  ∀ (this : Finite.{u_1 + 1} ↥S) (this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S })
    (this : Finite.{u_1 + 1} ↥f.toHom.range) (this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }),
    ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have₆ :
  ∀ (this : Finite.{u_1 + 1} ↥S) (this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S })
    (this_1 : Finite.{u_1 + 1} ↥f.toHom.range) (this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range }),
    f =
      Embedding.comp
        (Equiv.toEmbedding
          (StrongHomClass.toEquiv
            (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range) (Nonempty.some ⋯))))
        S.subtype
h :
  ∀ (this : Finite.{u_1 + 1} ↥S) (this : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S })
    (this_1 : Finite.{u_1 + 1} ↥f.toHom.range) (this_2 : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ f.toHom.range })
    (x : ↥S),
    Eq (α := M) ((f : (a : ↥S) → M) x : M)
      ((Embedding.comp
              (Equiv.toEmbedding
                (StrongHomClass.toEquiv
                  (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range)
                    (Nonempty.some ⋯))))
              S.subtype :
            (a : ↥S) → M)
          x :
        M)
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype

Tactic:
classical
    have : Finite S := hS.finite
    have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype
    have : Finite f.toHom.range := (((Substructure.fg_iff_structure_fg S).1 hS).range _).finite
    have : Infinite { x // x ∉ f.toHom.range } := ((Set.toFinite _).infinite_compl).to_subtype
    refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩
    ext x
    simp [Equiv.subtypeCongr]

Premises used: Equiv.subtypeCongr
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
h :
  ∀ (S : Bundled Language.empty.Structure),
    S ∈ Language.empty.age M ↔
      Membership.mem (γ := Set (Bundled Language.empty.Structure))
        {S : Bundled Language.empty.Structure | Finite.{u_1 + 1} (↑S : Type u_1)} S
⊢ Language.empty.age M = {S : Bundled Language.empty.Structure | Finite.{u_1 + 1} (↑S : Type u_1)}

Tactic:
ext S
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Bundled Language.empty.Structure
h : Finite.{u_1 + 1} (↑S : Type u_1) → Nonempty.{u_1 + 1} ((↑S : Type u_1) ↪[Language.empty] M)
⊢ S ∈ Language.empty.age M ↔
    Membership.mem (γ := Set (Bundled Language.empty.Structure))
      {S : Bundled Language.empty.Structure | Finite.{u_1 + 1} (↑S : Type u_1)} S

Tactic:
simp only [age, Structure.fg_iff_finite, mem_setOf_eq, and_iff_left_iff_imp]

Premises used: FirstOrder.Language.Structure.fg_iff_finite, FirstOrder.Language.age, Set.mem_setOf_eq, and_iff_left_iff_imp
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
S : Bundled Language.empty.Structure
hS : Finite.{u_1 + 1} (↑S : Type u_1)
⊢ Nonempty.{u_1 + 1} ((↑S : Type u_1) ↪[Language.empty] M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
have :
  ∀ (this : Language.empty.Structure (ULift.{w, 0} ℕ)),
    IsFraisse.{0, 0, w} (L := Language.empty) {S : Bundled Language.empty.Structure | Finite.{w + 1} (↑S : Type w)}
⊢ IsFraisse.{0, 0, w} (L := Language.empty) {S : Bundled Language.empty.Structure | Finite.{w + 1} (↑S : Type w)}

Tactic:
have : Language.empty.Structure (ULift ℕ : Type w) := emptyStructure
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
this : Language.empty.Structure (ULift.{w, 0} ℕ)
⊢ IsFraisse.{0, 0, w} (L := Language.empty) {S : Bundled Language.empty.Structure | Finite.{w + 1} (↑S : Type w)}

Tactic:
(isFraisseLimit_of_countable_infinite (ULift ℕ)).isFraisse

Premises used: FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, ULift, Nat, FirstOrder.Language.IsFraisseLimit.isFraisse
-- Module: Mathlib.ModelTheory.Fraisse
Goal:
this : Language.empty.Structure (ULift.{w, 0} ℕ)
⊢ IsFraisse.{0, 0, w} (L := Language.empty) {S : Bundled Language.empty.Structure | Finite.{w + 1} (↑S : Type w)}

Tactic:
exact (isFraisseLimit_of_countable_infinite (ULift ℕ)).isFraisse

Premises used: FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, ULift, Nat, FirstOrder.Language.IsFraisseLimit.isFraisse
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
⊢ graphRel.adj = graphRel.adj

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
inst : Language.graph.Structure V
⊢ V ⊨ Theory.simpleGraph ↔
    (Std.Irrefl fun (x y : V) ↦ RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) ↦ RelMap adj ![x, y]

Tactic:
simp [Theory.simpleGraph]

Premises used: FirstOrder.Language.Theory.simpleGraph
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
rw : (Std.Irrefl fun (x y : V) ↦ RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) ↦ RelMap adj ![x, y]
⊢ V ⊨ Theory.simpleGraph

Tactic:
rw [Theory.simpleGraph_model_iff]

Premises used: FirstOrder.Language.Theory.simpleGraph_model_iff
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
⊢ (Std.Irrefl fun (x y : V) ↦ RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) ↦ RelMap adj ![x, y]

Tactic:
⟨G.loopless, G.symm⟩

Premises used: SimpleGraph.symm, And.intro, SimpleGraph.loopless
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
⊢ (Std.Irrefl fun (x y : V) ↦ RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) ↦ RelMap adj ![x, y]

Tactic:
exact ⟨G.loopless, G.symm⟩
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
G : SimpleGraph V
Adj : ∀ (x x_1 : V), (Language.simpleGraphOfStructure V).Adj x x_1 ↔ G.Adj x x_1
⊢ Language.simpleGraphOfStructure V = G

Tactic:
ext
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
⊢ (Language.simpleGraphOfStructure V).Adj x x_1 ↔ G.Adj x x_1

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
funMap :
  ∀ (x : ℕ) (x_1 : Language.graph.Functions x) (x_2 : Fin x → V), Structure.funMap x_1 x_2 = Structure.funMap x_1 x_2
RelMap :
  ∀ (x : ℕ) (x_1 : Language.graph.Relations x) (x_2 : Fin x → V), Structure.RelMap x_1 x_2 ↔ Structure.RelMap x_1 x_2
⊢ (simpleGraphOfStructure V).structure = S

Tactic:
ext
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
f : Language.graph.Functions n
xs : Fin n → V
⊢ funMap f xs = funMap f xs

Tactic:
isEmptyElim f

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
f : Language.graph.Functions n
xs : Fin n → V
⊢ funMap f xs = funMap f xs

Tactic:
exact isEmptyElim f
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
x : ℕ
x_1 : Language.graph.Functions x
x_2 : Fin x → V
⊢ funMap x_1 x_2 = funMap x_1 x_2

Tactic:
case funMap n f xs =>
    exact isEmptyElim f

Premises used: FirstOrder.Language.Structure.funMap
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
rw : RelMap (L := Language.graph) graphRel.adj xs = RelMap (L := Language.graph) graphRel.adj xs
⊢ RelMap (L := Language.graph) graphRel.adj xs ↔ RelMap (L := Language.graph) graphRel.adj xs

Tactic:
rw [iff_eq_eq]

Premises used: iff_eq_eq
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
change : RelMap adj ![xs 0, xs 1] = RelMap (L := Language.graph) graphRel.adj xs
⊢ RelMap (L := Language.graph) graphRel.adj xs = RelMap (L := Language.graph) graphRel.adj xs

Tactic:
change RelMap adj ![xs 0, xs 1] = _

Premises used: FirstOrder.Language.Structure.RelMap, FirstOrder.Language.adj, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap adj ![xs 0, xs 1] = RelMap (L := Language.graph) graphRel.adj xs

Tactic:
congr rfl (funext ?_)

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
refine : ∀ (x : Fin (Nat.succ 1)), ![xs 0, xs 1] x = xs x
⊢ RelMap adj ![xs 0, xs 1] = RelMap (L := Language.graph) graphRel.adj xs

Tactic:
refine congr rfl (funext ?_)

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ ∀ (x : Fin (Nat.succ 1)), ![xs 0, xs 1] x = xs x

Tactic:
simp [Fin.forall_fin_two]

Premises used: Fin.forall_fin_two
-- Module: Mathlib.ModelTheory.Graph
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin n → V
⊢ RelMap r xs ↔ RelMap r xs

Tactic:
match n, r with
    | 2, .adj =>
      rw [iff_eq_eq]
      change RelMap adj ![xs 0, xs 1] = _
      refine congr rfl (funext ?_)
      simp [Fin.forall_fin_two]
-- Module: Mathlib.ModelTheory.Graph
Goal:
⊢ Theory.simpleGraph.IsSatisfiable

Tactic:
⟨@Theory.ModelType.of _ _ Unit (SimpleGraph.structure ⊥) _ _⟩

Premises used: FirstOrder.Language.Theory.IsSatisfiable, FirstOrder.Language.Theory.ModelType.of, Nonempty.intro, Unit
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
obtain :
  ∀ (Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n) (Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n)
    (h_fun : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onFunction = G.onFunction)
    (h_rel : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onRelation = G.onRelation),
    { onFunction := Ff, onRelation := Fr : L →ᴸ L' } = G
⊢ F = G

Tactic:
obtain ⟨Ff, Fr⟩ := F
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onRelation = G.onRelation
obtain :
  ∀ (Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n) (Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n)
    (h_fun :
      { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction)
    (h_rel :
      { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation),
    { onFunction := Ff, onRelation := Fr : L →ᴸ L' } = { onFunction := Gf, onRelation := Gr }
⊢ { onFunction := Ff, onRelation := Fr : L →ᴸ L' } = G

Tactic:
obtain ⟨Gf, Gr⟩ := G
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
simp : Ff = Gf ∧ Fr = Gr
⊢ { onFunction := Ff, onRelation := Fr : L →ᴸ L' } = { onFunction := Gf, onRelation := Gr }

Tactic:
simp only [mk.injEq]

Premises used: FirstOrder.Language.LHom.mk.injEq
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr

Tactic:
And.intro h_fun h_rel

Premises used: And.intro