awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
⊢ Hom.range (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) = ⨆ (i : ι), (g i).toHom.range
have simp_rw : Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) ⊤ =
  ⨆ (i : ι), Substructure.map (g i).toHom ⊤
Tactic: simp_rw [Hom.range_eq_map]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
⊢ Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) ⊤ =
    ⨆ (i : ι), Substructure.map (g i).toHom ⊤
have rw : Eq.{u₁ + 1} (α := L.Substructure P)
  (⨆ (i : ι),
    Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg))
      (Hom.range (Embedding.toHom (of L ι G f i))))
  (⨆ (i : ι), Substructure.map (g i).toHom ⊤)
Tactic: rw [← iSup_range_of_eq_top, Substructure.map_iSup]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
⊢ Eq.{u₁ + 1} (α := L.Substructure P)
    (⨆ (i : ι),
      Substructure.map (M := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg))
        (Hom.range (Embedding.toHom (of L ι G f i))))
    (⨆ (i : ι), Substructure.map (g i).toHom ⊤)
have simp_rw : Eq.{u₁ + 1} (α := L.Substructure P)
  (⨆ (i : ι),
    Substructure.map
      (Hom.comp (N := DirectLimit G f) (Embedding.toHom (lift L ι G f g Hg)) (Embedding.toHom (of L ι G f i))) ⊤)
  (⨆ (i : ι), Substructure.map (g i).toHom ⊤)
Tactic: simp_rw [Hom.range_eq_map, Substructure.map_map]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
⊢ ∃ (a : DirectLimit G f), (F : (a : DirectLimit G f) → DirectLimit G' f') a = x
have mk : ∀ (i : ι) (pre_x : G' i),
  ∃ (a : DirectLimit G f),
    Eq (α := DirectLimit G' f') ((F : (a : DirectLimit G f) → DirectLimit G' f') a : DirectLimit G' f')
      (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
        Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
Tactic: rcases x with ⟨i, pre_x⟩
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
i : ι
pre_x : G' i
⊢ ∃ (a : DirectLimit G f),
    Eq (α := DirectLimit G' f') ((F : (a : DirectLimit G f) → DirectLimit G' f') a : DirectLimit G' f')
      (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
        Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
have h : Eq (α := DirectLimit G' f')
  ((F : (a : DirectLimit G f) → DirectLimit G' f')
      ((of L ι G f i : (a : G i) → DirectLimit G f) (((g i).symm : (a : G' i) → G i) pre_x)) :
    DirectLimit G' f')
  (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
    Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
Tactic: use of L _ G f i ((g i).symm pre_x)
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
i : ι
pre_x : G' i
⊢ Eq (α := DirectLimit G' f')
    ((F : (a : DirectLimit G f) → DirectLimit G' f')
        ((of L ι G f i : (a : G i) → DirectLimit G f) (((g i).symm : (a : G' i) → G i) pre_x)) :
      DirectLimit G' f')
    (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
      Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
have h : Eq (α := DirectLimit G' f') ((of L ι G' f' i : (a : G' i) → DirectLimit G' f') pre_x : DirectLimit G' f')
  (Quot.mk (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop) (Sigma.mk (β := fun (i : ι) ↦ G' i) i pre_x) :
    Quot (α := Σˣ (G := G') f') (⇑(setoid G' f') : Σˣ f' → Σˣ f' → Prop))
Tactic: simp only [F, U, lift_of, Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (hypothesis)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
inst_4 : Nonempty ι
P : Type u₁
inst_5 : L.Structure P
g_1 : (i : ι) → Embedding.{u_1, u_2, w, u₁} L (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u₁ + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type w'
inst_6 : (i : ι) → Structure.{u_1, u_2, w'} L (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → Equiv.{u_1, u_2, w, w'} L (G i) (G' i)
inst_7 : DirectedSystem G' fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G' i) → G' j)
H_commuting :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{w' + 1} (α := G' j) ((g j : (a : G j) → G' j) ((f i j hij : (a : G i) → G j) x) : G' j)
      ((f' i j hij : (a : G' i) → G' j) ((g i : (a : G i) → G' i) x : G' i) : G' j)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun (i : ι) ↦ Embedding.comp (of L ι G' f' i) (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
⊢ DirectLimit G f ≃[L] DirectLimit G' f'
have surj_f : Function.Surjective (α := DirectLimit G f) (β := DirectLimit G' f') (⇑F : (a : DirectLimit G f) → DirectLimit G' f')
Tactic: have surj_f : Function.Surjective F := by
    intro x
    rcases x with ⟨i, pre_x⟩
    use of L _ G f i ((g i).symm pre_x)
    simp only [F, U, lift_of, Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.apply_symm_apply]
    rfl
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ CG L (DirectLimit G f)
have refine_1 : Set.Countable (α := DirectLimit G f)
  (⋃ (i : ι),
    image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
      (Classical.choose (p := fun (x : Set (G i)) ↦
        x.Countable ∧
          Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
        sorry))
Tactic: refine ⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
refine_1 :
  Set.Countable (α := DirectLimit G f)
    (⋃ (i : ι),
      image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          ⋯))
⊢ CG L (DirectLimit G f)
have refine_2 : Eq (α := L.Substructure (DirectLimit G f))
  (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
    (⋃ (i : ι),
      image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          sorry)))
  ⊤
Tactic: refine ⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ Eq (α := L.Substructure (DirectLimit G f))
    (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (⋃ (i : ι),
        image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
    ⊤
have refine_2 : LE.le (α := L.Substructure (DirectLimit G f)) ⊤
  (⨆ (i : ι),
    LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
      (image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          sorry)))
Tactic: rw [eq_top_iff, Substructure.closure_iUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ LE.le (α := L.Substructure (DirectLimit G f)) ⊤
    (⨆ (i : ι),
      LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
        (image (α := G i) (⇑(of L ι G f i) : (a : G i) → DirectLimit G f)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
have refine_2 : LE.le (α := L.Substructure (DirectLimit G f)) ⊤
  (⨆ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
      (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
        (Classical.choose (p := fun (x : Set (G i)) ↦
          x.Countable ∧
            Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
          sorry)))
Tactic: simp_rw [← Embedding.coe_toHom, Substructure.closure_image]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ LE.le (α := L.Substructure (DirectLimit G f)) ⊤
    (⨆ (i : ι),
      Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)))
have refine_2 : ∀ (b : L.Substructure (DirectLimit G f)),
  (∀ (i : ι),
      Substructure.map (Embedding.toHom (of L ι G f i))
          (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
            (Classical.choose (p := fun (x : Set (G i)) ↦
              x.Countable ∧
                Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
              sorry)) ≤
        b) →
    ⊤ ≤ b
Tactic: rw [le_iSup_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
⊢ x ∈ S
have refine_2 : (out x).snd (β := fun (i : ι) ↦ G i) ∈
  (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
        (Classical.choose (p := fun (x_1 : Set (G ((out x).fst (β := fun (i : ι) ↦ G i)))) ↦
          x_1.Countable ∧
            Eq (α := L.Substructure (G ((out x).fst (β := fun (i : ι) ↦ G i))))
              (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x_1) ⊤)
          sorry)) :
    Set (G (out x).fst))
Tactic: refine hS (out x).1 ⟨(out x).2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
refine_2 :
  (out x).snd (β := fun (i : ι) ↦ G i) ∈
    (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x_1 : Set (G ((out x).fst (β := fun (i : ι) ↦ G i)))) ↦
            x_1.Countable ∧
              Eq (α := L.Substructure (G ((out x).fst (β := fun (i : ι) ↦ G i))))
                (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x_1) ⊤)
            ⋯)) :
      Set (G (out x).fst))
⊢ x ∈ S
have refine_2₁ : (Embedding.toHom (of L ι G f ((out x).fst (β := fun (i : ι) ↦ G i))) : (a : G (out x).fst) → DirectLimit G f)
    ((out x).snd (β := fun (i : ι) ↦ G i)) =
  x
Tactic: refine hS (out x).1 ⟨(out x).2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type u_1
inst : Countable ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
G : ι → Type w
inst_4 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG.{w, u_2, u_3} L (G i)
inst_5 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
S : L.Substructure (DirectLimit G f)
hS :
  ∀ (i : ι),
    Substructure.map (Embedding.toHom (of L ι G f i))
        (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x : Set (G i)) ↦
            x.Countable ∧
              Eq (α := L.Substructure (G i)) (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x) ⊤)
            ⋯)) ≤
      S
x : DirectLimit G f
h_1 : Membership.mem (γ := L.Substructure (DirectLimit G f)) ⊤ x
out : Quotient (setoid G f) → Σˣ (G := G) f := Quotient.out
⊢ (out x).snd (β := fun (i : ι) ↦ G i) ∈
    (↑(LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L)
          (Classical.choose (p := fun (x_1 : Set (G ((out x).fst (β := fun (i : ι) ↦ G i)))) ↦
            x_1.Countable ∧
              Eq (α := L.Substructure (G ((out x).fst (β := fun (i : ι) ↦ G i))))
                (LowerAdjoint.toFun (u := SetLike.coe) (Substructure.closure L) x_1) ⊤)
            ⋯)) :
      Set (G (out x).fst))
have refine_2 : (out x).snd (β := fun (i : ι) ↦ G i) ∈ (↑⊤ : Set (G (out x).fst))
Tactic: rw [(Classical.choose_spec (h (out x).1).out).2]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
M : Type u_1
inst_3 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
⊢ Hom.range (M :=
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
      (Embedding.toHom (liftInclusion S)) =
    ⨆ (i : ι), (S : (a : ι) → L.Substructure M) i
have simp_rw : Hom.range (M :=
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry)
    (Embedding.toHom
      (lift L ι (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion sorry)
        (fun (x : ι) ↦ Substructure.subtype ((S : (a : ι) → L.Substructure M) x)) sorry)) =
  ⨆ (i : ι), (S : (a : ι) → L.Substructure M) i
Tactic: simp_rw [liftInclusion, range_lift, Substructure.range_subtype]
-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
M : Type u_1
inst_3 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
simp_rw :
  Hom.range (M :=
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
      (Embedding.toHom
        (lift L ι (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
          (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
          (fun (x : ι) ↦ Substructure.subtype ((S : (a : ι) → L.Substructure M) x)) ⋯)) =
    ⨆ (i : ι), (S : (a : ι) → L.Substructure M) i
⊢ Hom.range (M :=
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
      (Embedding.toHom (liftInclusion S)) =
    ⨆ (i : ι), (S : (a : ι) → L.Substructure M) i
have simp_rw₁ : Eq.{u_1 + 1} (α := L.Substructure M)
  (⨆ (i : ι),
    Hom.range (M := ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      (Embedding.toHom (Substructure.subtype ((S : (a : ι) → L.Substructure M) i))))
  (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
Tactic: simp_rw [liftInclusion, range_lift, Substructure.range_subtype]