awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine_2 : lift.{max (max u v) w, w'} κ ≤
  lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
Tactic: rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max (max u v) w, w'} κ ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine_2₁ : lift.{max u v, max w w'} (lift.{w, w'} κ) ≤
  lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
Tactic: rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max (max u v) w, w'} κ ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₁ :
  lift.{max u v, max w w'} (lift.{w, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine_2₂ : lift.{max u v, max w w'} #(↑s' : Type (max w w')) ≤
  lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
Tactic: rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max (max u v) w, w'} κ ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₁ :
  lift.{max u v, max w w'} (lift.{w, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₂ :
  lift.{max u v, max w w'} #(↑s' : Type (max w w')) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine_2₃ : lift.{max u v, max w w'} (lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)) ≤
  lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
Tactic: rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max (max u v) w, w'} κ ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₁ :
  lift.{max u v, max w w'} (lift.{w, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₂ :
  lift.{max u v, max w w'} #(↑s' : Type (max w w')) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₃ :
  lift.{max u v, max w w'} (lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine_2₄ : lift.{max w' u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
  lift.{max w' u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
Tactic: rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ ℵ₀ ≤ lift.{max u v, w} #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine : ℵ₀ ≤ lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
Tactic: refine _root_.trans ?_ (lift_le.2 (mk_le_mk_of_subset Set.subset_union_right))
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
p q : L.Substructure M
h : (↑p : Set M) = (↑q : Set M)
⊢ p = q
have mk : ∀ (carrier : Set M) (fun_mem : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier)
  (h : (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) = (↑q : Set M)),
  { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
q : L.Substructure M
carrier : Set M
fun_mem : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier
h : (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) = (↑q : Set M)
⊢ { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = q
have mk : ∀ (carrier_1 : Set M) (fun_mem_1 : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier_1)
  (h :
    (↑{ carrier := carrier, fun_mem := @fun_mem : L.Substructure M } : Set M) =
      (↑{ carrier := carrier_1, fun_mem := @fun_mem_1 : L.Substructure M } : Set M)),
  { carrier := carrier, fun_mem := @fun_mem : L.Substructure M } = { carrier := carrier_1, fun_mem := @fun_mem_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
t : L.Term α
xs : α → M
h : ∀ (a : α), xs a ∈ S
⊢ realize xs t ∈ S
have var : ∀ (a : α), realize.{u, v, w, u_3} (L := L) xs (var a) ∈ S
Tactic: induction t with
  | var a => exact h a
  | func f ts ih => exact Substructure.fun_mem _ _ _ ih
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
α : Type u_3
t : L.Term α
xs : α → M
h : ∀ (a : α), xs a ∈ S
var : ∀ (a : α), realize.{u, v, w, u_3} (L := L) xs (Language.var a) ∈ S
⊢ realize xs t ∈ S
have func : ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term α) (ih : ∀ (a : Fin l), realize xs (ts a) ∈ S),
  realize xs (func f ts) ∈ S
Tactic: induction t with
  | var a => exact h a
  | func f ts ih => exact Substructure.fun_mem _ _ _ ih
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
⊢ ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
have pos : ∀ (h : t ∈ s), ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
Tactic: by_cases h : t ∈ s
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
pos :
  ∀ (h : t ∈ s),
    ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
⊢ ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
have neg : ∀ (h : t ∉ s), ClosedUnder.{u, v, w} (M := M) f ((fun (t : L.Substructure M) ↦ (⋂ (_ : t ∈ s), (↑t : Set M) : Set M)) t)
Tactic: by_cases h : t ∈ s
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
n : ℕ
f : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    Membership.mem (γ := Set M)
      (range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) (x i)
⊢ Membership.mem (γ := Set M)
    (range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
    (funMap f x)
have hx₁ : ∀ (i : Fin n),
  ∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x i
Tactic: simp only [mem_range] at *
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
n : ℕ
f : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    ∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x i
⊢ ∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = funMap f x
have refine : Term.realize (α := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))
    (func f fun (i : Fin n) ↦
      Classical.choose (p := fun (x_1 : Term.{u, v, w} L { x : M // x ∈ s }) ↦
        Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) x_1 = x i) sorry) =
  funMap f x
Tactic: refine ⟨func f fun i => Classical.choose (hx i), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) =
    range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))
have change : (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) = (↑S : Set M)
Tactic: change _ = (S : Set M)
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
⊢ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) = (↑S : Set M)
have rw : LowerAdjoint.toFun (u := SetLike.coe) (closure L) s = S
Tactic: rw [← SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
S : L.Substructure M :=
  { carrier := range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
    fun_mem := ⋯ }
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) s = S
have refine : ∀ (S' : L.Substructure M)
  (hS' : Membership.mem (γ := Set (L.Substructure M)) {S : L.Substructure M | s ⊆ (↑S : Set M)} S'), S ≤ S'
Tactic: refine closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
S : L.Substructure M
s : Set M
inst_3 : Small.{u, w} (↑s : Type w)
⊢ Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
have rw : Small.{u, w}
  (↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) : Type w)
Tactic: rw [← SetLike.coe_sort_coe, Substructure.coe_closure_eq_range_term_realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
x : M
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
have rw : x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔
  ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
Tactic: rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
x : M
rw :
  x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
have rw₁ : Membership.mem (γ := Set M)
    (range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
  ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
Tactic: rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
x : M
rw :
  x ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
rw₁ :
  Membership.mem (γ := Set M)
      (range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x ↔
    ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
have rw₂ : (∃ (y : Term.{u, v, w} L { x : M // x ∈ s }), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) y = x) ↔
  ∃ (t : Term.{u, v, w} L (↑s : Type w)), Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)) t = x
Tactic: rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤ #(Term.{u, v, w} L (↑s : Type w))
have rw : lift.{max u w, w}
    #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
        Type w) ≤
  #(Term.{u, v, w} L (↑s : Type w))
Tactic: rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ lift.{max u w, w}
      #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
          Type w) ≤
    #(Term.{u, v, w} L (↑s : Type w))
have rw : lift.{max u w, w}
    #(↑(range (ι := Term.{u, v, w} L { x : M // x ∈ s }) (Term.realize (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) :
        Type w) ≤
  lift.{w, max u w} #(Term.{u, v, w} L (↑s : Type w))
Tactic: rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ lift.{u, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤
    max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
have rw : lift.{max w u, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤
  max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
Tactic: rw [← lift_umax]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ lift.{max w u, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
have refine : max ℵ₀ #(Sum.{w, u} (↑s : Type w) ((i : ℕ) × L.Functions i)) ≤
  max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
Tactic: refine lift_card_closure_le_card_term.trans (Term.card_le.trans ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ max ℵ₀ #(Sum.{w, u} (↑s : Type w) ((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
have rw : max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i)) ≤
  max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
Tactic: rw [mk_sum, lift_umax.{w, u}]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
rw :
  max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
⊢ max ℵ₀ #(Sum.{w, u} (↑s : Type w) ((i : ℕ) × L.Functions i)) ≤
    max ℵ₀ (lift.{max w u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
have rw₁ : max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i)) ≤
  max ℵ₀ (lift.{u, w} #(↑s : Type w) + lift.{w, u} #((i : ℕ) × L.Functions i))
Tactic: rw [mk_sum, lift_umax.{w, u}]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s ↔
    ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
have refine_1 : ∀ (h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s) (n : ℕ)
  (f : L.Functions n), ClosedUnder f s
Tactic: refine ⟨fun h n f => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
refine_1 :
  ∀ (h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s) (n : ℕ)
    (f : L.Functions n), ClosedUnder f s
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s ↔
    ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
have refine_2 : ∀ (h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s),
  Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
Tactic: refine ⟨fun h n f => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
n : ℕ
f : L.Functions n
⊢ ClosedUnder f s
have refine_1 : ClosedUnder f (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) s
have h' : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) { carrier := s, fun_mem := sorry }
Tactic: have h' : closure L s = ⟨s, h⟩ := closure_eq_of_le (refl _) subset_closure
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : L.IsRelational
s : Set M
m : M
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) m ↔ m ∈ s
have rw : m ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔ m ∈ s
Tactic: rw [← SetLike.mem_coe, closure_eq_of_isRelational]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : L.IsRelational
s : Set M
m : M
rw : m ∈ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) : Set M) ↔ m ∈ s
⊢ Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) m ↔ m ∈ s
have rw₁ : m ∈ s ↔ m ∈ s
Tactic: rw [← SetLike.mem_coe, closure_eq_of_isRelational]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
inst_1 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
h : s.Countable
⊢ Countable.{w + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
have this : Countable.{w + 1} (↑s : Type w)
Tactic: haveI : Countable s := h.to_subtype
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
inst_1 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
h : s.Countable
this : Countable.{w + 1} (↑s : Type w)
⊢ Countable.{w + 1} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)
have rw : lift.{max u w, w} #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ≤ ℵ₀
Tactic: rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
p : M → Prop
x : M
s : Set M
hs : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) ⊤
Hs : ∀ x ∈ s, p x
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f (setOf p)
⊢ p x
have have : ∀
  (this :
    ∀ (x : M), Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x → p x),
  p x
Tactic: have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun