awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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 ⋯)
⊢ (↑(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 ⋯)) =
    (↑(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
have h : ∀ (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 sorry)) :
          (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: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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 := ⊥
⊢ Nonempty.{w + 1} (M ≃[L] N)
have S_fg : Structure.FG.{w, u, v} L ↥S
Tactic: have S_fg : FG L S := (fg_iff_structure_fg _).1 Substructure.fg_bot
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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 N
have rw : { α := ↥S, str := inferInstance } ∈ L.age M
Tactic: rw [hN.age, ← hM.age]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ Nonempty.{w + 1} (M ≃[L] N)
have obtain : Structure.FG.{w, u, v} L (↑{ α := ↥S, str := inferInstance } : Type w) →
  ∀ (emb_S : ↥S ↪[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 _⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have this : Finite.{u_1 + 1} ↥S
Tactic: have : Finite S := hS.finite
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have this₁ : Infinite.{max 1 (u_1 + 1)} { x : M // x ∉ S }
Tactic: have : Infinite { x // x ∉ S } := ((Set.toFinite _).infinite_compl).to_subtype
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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 }
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have this₁ : Finite.{u_1 + 1} ↥f.toHom.range
Tactic: have : Finite f.toHom.range := (((Substructure.fg_iff_structure_fg S).1 hS).range _).finite
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have this₁ : 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
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
have refine : f =
  Embedding.comp
    (Equiv.toEmbedding
      (StrongHomClass.toEquiv
        (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range) (Nonempty.some sorry))))
    S.subtype
Tactic: refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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 }
⊢ f =
    Embedding.comp
      (Equiv.toEmbedding
        (StrongHomClass.toEquiv
          (f.equivRange.subtypeCongr (p := Membership.mem S) (q := Membership.mem f.toHom.range) (Nonempty.some ⋯))))
      S.subtype
have 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 sorry))))
            S.subtype :
          (a : ↥S) → M)
        x :
      M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have have : ∀ (this : Finite.{u_1 + 1} ↥S), ∃ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have 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
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have 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
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have 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
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have 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 sorry))))
      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]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
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
⊢ ∃ (g : M ≃[Language.empty] M), f = g.toEmbedding.comp S.subtype
have 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 sorry))))
            S.subtype :
          (a : ↥S) → M)
        x :
      M)
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
⊢ Language.empty.age M = {S : Bundled Language.empty.Structure | Finite.{u_1 + 1} (↑S : Type u_1)}
have 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
Tactic: ext S
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
M : Type u_1
inst : Countable M
inst_1 : Infinite M
inst_2 : Language.empty.Structure M
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
have h : Finite.{u_1 + 1} (↑S : Type u_1) → Nonempty.{u_1 + 1} ((↑S : Type u_1) ↪[Language.empty] M)
Tactic: simp only [age, Structure.fg_iff_finite, mem_setOf_eq, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
⊢ IsFraisse.{0, 0, w} (L := Language.empty) {S : Bundled Language.empty.Structure | Finite.{w + 1} (↑S : Type w)}
have 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)}
Tactic: have : Language.empty.Structure (ULift ℕ : Type w) := emptyStructure
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
Goal:
V : Type u
n : ℕ
G : SimpleGraph V
this : Language.graph.Structure V := G.structure
⊢ V ⊨ Theory.simpleGraph
have rw : (Std.Irrefl fun (x y : V) ↦ RelMap adj ![x, y]) ∧ Symmetric fun (x y : V) ↦ RelMap adj ![x, y]
Tactic: rw [Theory.simpleGraph_model_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ Language.simpleGraphOfStructure V = G
have Adj : ∀ (x x_1 : V), (Language.simpleGraphOfStructure V).Adj x x_1 ↔ G.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
⊢ (simpleGraphOfStructure V).structure = S
have funMap : ∀ (x : ℕ) (x_1 : Language.graph.Functions x) (x_2 : Fin x → V), funMap x_1 x_2 = funMap x_1 x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
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
⊢ (simpleGraphOfStructure V).structure = S
have RelMap : ∀ (x : ℕ) (x_1 : Language.graph.Relations x) (x_2 : Fin x → V), RelMap x_1 x_2 ↔ RelMap x_1 x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap (L := Language.graph) graphRel.adj xs ↔ RelMap (L := Language.graph) graphRel.adj xs
have rw : RelMap (L := Language.graph) graphRel.adj xs = RelMap (L := Language.graph) graphRel.adj xs
Tactic: rw [iff_eq_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
Goal:
V : Type u
S : Language.graph.Structure V
inst : V ⊨ Theory.simpleGraph
n : ℕ
r : Language.graph.Relations n
xs : Fin 2 → V
⊢ RelMap (L := Language.graph) graphRel.adj xs = RelMap (L := Language.graph) graphRel.adj xs
have change : RelMap adj ![xs 0, xs 1] = RelMap (L := Language.graph) graphRel.adj xs
Tactic: change RelMap adj ![xs 0, xs 1] = _
-- Lean 4 proof step from Mathlib.ModelTheory.Graph (goal)
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
have refine : ∀ (x : Fin (Nat.succ 1)), ![xs 0, xs 1] x = xs x
Tactic: refine congr rfl (funext ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
⊢ F = G
have 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
Tactic: obtain ⟨Ff, Fr⟩ := F
Cleared hypotheses: F, h_fun, h_rel
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
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
⊢ { onFunction := Ff, onRelation := Fr : L →ᴸ L' } = G
have 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 }
Tactic: obtain ⟨Gf, Gr⟩ := G
Cleared hypotheses: G, h_fun, h_rel
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
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
⊢ { onFunction := Ff, onRelation := Fr : L →ᴸ L' } = { onFunction := Gf, onRelation := Gr }
have simp : Ff = Gf ∧ Fr = Gr
Tactic: simp only [mk.injEq]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
F : L →ᴸ L'
⊢ LHom.id L' ∘ᴸ F = F
have mk : ∀ (onFunction : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n) (onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n),
  LHom.id L' ∘ᴸ { onFunction := onFunction, onRelation := onRelation : L →ᴸ L' } =
    { onFunction := onFunction, onRelation := onRelation }
Tactic: cases F
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
F : L →ᴸ L'
⊢ F ∘ᴸ LHom.id L = F
have mk : ∀ (onFunction : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n) (onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n),
  { onFunction := onFunction, onRelation := onRelation : L →ᴸ L' } ∘ᴸ LHom.id L =
    { onFunction := onFunction, onRelation := onRelation }
Tactic: cases F
Cleared hypotheses: F