awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have obtain : ∀ (F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid) (hF : Quotient.mk' '' K = range F),
  ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
Tactic: obtain ⟨F, hF⟩ := hc.exists_eq_range (hn.image _)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF : Quotient.mk' '' K = range F
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have hF₁ : ∀ (a : Bundled L.Structure),
  (∃ x ∈ K, Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' x) ⟦a⟧) ↔ ∃ (y : ℕ), F y = ⟦a⟧
Tactic: simp only [Set.ext_iff, Quotient.forall, mem_image, mem_range] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Eq (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' x) ⟦a⟧) ↔ ∃ (y : ℕ), F y = ⟦a⟧
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have hF₁ : ∀ (a : Bundled L.Structure), (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
Tactic: simp_rw [Quotient.eq_mk_iff_out] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
n : ℕ
⊢ (F n).out ∈ K
have obtain : ∀ (P : Bundled L.Structure) (hP1 : P ∈ K) (hP2 : Quotient.out (s := equivSetoid) (Quotient.mk' P) ≈ (F n).out),
  (F n).out ∈ K
Tactic: obtain ⟨P, hP1, hP2⟩ := (hF (F n).out).2 ⟨n, Setoid.refl _⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
n : ℕ
P : Bundled L.Structure
hP1 : P ∈ K
hP2 : Quotient.out (s := equivSetoid) (Quotient.mk' P) ≈ (F n).out
⊢ (F n).out ∈ K
have hP2₁ : P ≈ (F n).out
Tactic: replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
Cleared hypotheses: hP2
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have hF' : ∀ (n : ℕ), (F n).out ∈ K
Tactic: have hF' : ∀ n : ℕ, (F n).out ∈ K := by
    intro n
    obtain ⟨P, hP1, hP2⟩ := (hF (F n).out).2 ⟨n, Setoid.refl _⟩
    -- Porting note: fix hP2 because `Quotient.out (Quotient.mk' x) ≈ a` was not simplified
    -- to `x ≈ a` in hF
    replace hP2 := Setoid.trans (Setoid.symm (Quotient.mk_out P)) hP2
    exact (hp.is_equiv_invariant_of_fg fg _ _ hP2).1 hP1
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have choose : ∀ (P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure)
  (hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K)
  (hP :
    ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
      (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
        (P N n))
  (hFP :
    ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
      (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)),
  ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
Tactic: choose P hPK hP hFP using fun (N : K) (n : ℕ) => jep N N.2 (F (n + 1)).out (hF' _)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have refine_1 : Structure.CG.{w, u, v} L
  (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w)
Tactic: refine ⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
refine_1 :
  Structure.CG.{w, u, v} L
    (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w)
⊢ ∃ (M : Bundled L.Structure), Structure.CG.{w, u, v} L (↑M : Type w) ∧ L.age (↑M : Type w) = K
have refine_2 : L.age (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w) = K
Tactic: refine ⟨Bundled.of (@DirectLimit L _ _ (fun n ↦ (G n).val) _ f _ _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
⊢ L.age (↑(Bundled.of (DirectLimit (fun (n : ℕ) ↦ (↑(↑(G n) : Bundled L.Structure) : Type w)) f)) : Type w) = K
have refine_2 : ∀ (N : Bundled L.Structure) (KN : N ∈ K),
  Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
Tactic: refine (age_directLimit (fun n ↦ (G n).val) f).trans
      (subset_antisymm (iUnion_subset fun n N hN => hp (G n).val (G n).2 hN) fun N KN => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (hypothesis)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
⊢ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
have this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
Tactic: have : Quotient.out (Quotient.mk' N) ≈ N := Quotient.eq_mk_iff_out.mp rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
⊢ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
have refine_2 : ∀ (n : ℕ) (e : (↑(F n).out : Type w) ≃[L] (↑N : Type w)),
  Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
Tactic: obtain ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, this⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
n : ℕ
e : (↑(F n).out : Type w) ≃[L] (↑N : Type w)
⊢ Membership.mem (γ := Set (Bundled L.Structure)) (⋃ (i : ℕ), L.age (↑(↑(G i) : Bundled L.Structure) : Type w)) N
have refine_2 : (↑(F n).out : Type w) ↪[L] (↑(↑(G n) : Bundled L.Structure) : Type w)
Tactic: refine mem_iUnion_of_mem n ⟨fg _ KN, ⟨Embedding.comp ?_ e.symm.toEmbedding⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
n : ℕ
e : (↑(F n).out : Type w) ≃[L] (↑N : Type w)
⊢ (↑(F n).out : Type w) ↪[L] (↑(↑(G n) : Bundled L.Structure) : Type w)
have refine_2 : (e : (↑(F 0).out : Type w) ≃[L] (↑N : Type w)) → (↑(F 0).out : Type w) ↪[L] (↑(↑(G 0) : Bundled L.Structure) : Type w)
Tactic: rcases n with - | n
Cleared hypotheses: n, e
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
n : ℕ
e : (↑(F n).out : Type w) ≃[L] (↑N : Type w)
refine_2 :
  (e : (↑(F 0).out : Type w) ≃[L] (↑N : Type w)) → (↑(F 0).out : Type w) ↪[L] (↑(↑(G 0) : Bundled L.Structure) : Type w)
⊢ (↑(F n).out : Type w) ↪[L] (↑(↑(G n) : Bundled L.Structure) : Type w)
have refine_2₁ : (n : ℕ) →
  (e : (↑(F (n + 1)).out : Type w) ≃[L] (↑N : Type w)) →
    (↑(F (n + 1)).out : Type w) ↪[L] (↑(↑(G (n + 1)) : Bundled L.Structure) : Type w)
Tactic: rcases n with - | n
Cleared hypotheses: n, e
-- Lean 4 proof step from Mathlib.ModelTheory.Fraisse (goal)
Goal:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : Set.Countable (α := Quotient (α := Bundled L.Structure) equivSetoid) (Quotient.mk' '' K)
fg : ∀ M ∈ K, Structure.FG.{w, u, v} L (↑M : Type w)
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient (α := Bundled L.Structure) equivSetoid
hF :
  ∀ (a : Bundled L.Structure),
    (∃ x ∈ K, Quotient.out (s := equivSetoid) (Quotient.mk' x) ≈ a) ↔ ∃ (y : ℕ), (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : (N : (↑K : Type (max (max u v) (w + 1)))) → (n : ℕ) → Bundled L.Structure
hPK : ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ), P N n ∈ K
hP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (↑N : Bundled L.Structure)
      (P N n)
hFP :
  ∀ (N : (↑K : Type (max (max u v) (w + 1)))) (n : ℕ),
    (fun (M N : Bundled L.Structure) ↦ Nonempty.{w + 1} ((↑M : Type w) ↪[L] (↑N : Type w))) (F (n + 1)).out (P N n)
G : ℕ → (↑K : Type (max (max u v) (w + 1))) :=
  Nat.rec (motive := fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1))))
    (Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (F 0).out ⋯)
    fun (n : ℕ) (N : (fun (x : ℕ) ↦ (↑K : Type (max (max u v) (w + 1)))) n) ↦
    Subtype.mk (p := fun (x : Bundled L.Structure) ↦ x ∈ K) (P N n) ⋯
f : (i j : ℕ) → i ≤ j → (↑(↑(G i) : Bundled L.Structure) : Type w) ↪[L] (↑(↑(G j) : Bundled L.Structure) : Type w) :=
  DirectedSystem.natLERec (G' := fun (i : ℕ) ↦ (↑(↑(G i) : Bundled L.Structure) : Type w)) fun (n : ℕ) ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : Quotient.out (s := equivSetoid) (Quotient.mk' N) ≈ N
e : (↑(F 0).out : Type w) ≃[L] (↑N : Type w)
⊢ (↑(F 0).out : Type w) ↪[L] (↑(↑(G 0) : Bundled L.Structure) : Type w)
have refine_2 : (↑(F 0).out : Type w) ↪[L] (↑(F 0).out : Type w)
Tactic: dsimp [G]