awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Small.{u, w} ↥⊥
have rw : Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅)
Tactic: rw [← closure_empty]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
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
⊢ Small.{u, w} ↥(LowerAdjoint.toFun (u := SetLike.coe) (closure L) ∅)
have this : Small.{u, w} (↑∅ : Type w)
Tactic: haveI : Small.{u} (∅ : Set M) := small_subsingleton _
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ Eq.{w + 1} (α := L.Substructure M) (⨆ (i : ι), S i)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M)))
have simp_rw : Eq.{w + 1} (α := L.Substructure M) (⨆ (i : ι), S i)
  (⨆ (i : ι), LowerAdjoint.toFun (u := SetLike.coe) (closure L) (↑(S i) : Set M))
Tactic: simp_rw [closure_iUnion, closure_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have refine : Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
Tactic: refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := L.Substructure M) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
have suffices : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M)))
    x →
  ∃ (i : ι), x ∈ S i
Tactic: suffices x ∈ closure L (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ Membership.mem (γ := L.Substructure M)
      (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x →
    ∃ (i : ι), x ∈ S i
have refine : ∀
  (hx :
    Membership.mem (γ := L.Substructure M)
      (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x)
  {n : ℕ} (f : L.Functions n) (v : Fin n → M)
  (hC : ∀ (i : Fin n), Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (v i)),
  Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (funMap f v)
Tactic: refine fun hx ↦ closure_induction hx (fun _ ↦ mem_iUnion.1) (fun f v hC ↦ ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
hx :
  Membership.mem (γ := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x
n : ℕ
f : L.Functions n
v : Fin n → M
hC : ∀ (i : Fin n), Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (v i)
⊢ Membership.mem (γ := Set M) {x : M | ∃ (i : ι), x ∈ S i} (funMap f v)
have hC₁ : ∀ (i : Fin n), ∃ (i_1 : ι), v i ∈ S i_1
Tactic: simp_rw [Set.mem_setOf] at *
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
hx :
  Membership.mem (γ := L.Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (⋃ (i : ι), (↑(S i) : Set M))) x
n : ℕ
f : L.Functions n
v : Fin n → M
hC : ∀ (i : Fin n), ∃ (i_1 : ι), v i ∈ S i_1
⊢ ∃ (i : ι), funMap f v ∈ S i
have have : ∀ (i : ι) (hi : ∀ (i_1 : Fin n), S (Classical.choose (p := fun (x : ι) ↦ v i_1 ∈ S x) sorry) ≤ S i),
  ∃ (i : ι), funMap f v ∈ S i
Tactic: have ⟨i, hi⟩ := hS.finite_le (fun i ↦ Classical.choose (hC i))
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : Set (L.Substructure M)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : L.Substructure M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
have this : Nonempty.{w + 1} (↑S : Type w)
Tactic: haveI : Nonempty S := Sne.to_subtype
-- 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 : IsEmpty.{u + 1} L.Constants
⊢ IsEmpty.{w + 1} ↥⊥
have refine : ∀ (x : M), x ∉ ⊥
Tactic: refine (isEmpty_subtype _).2 (fun x => ?_)
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
⊢ Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) ∅
have rw : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder.{u, v, w} (M := M) f ∅
Tactic: rw [mem_closed_iff]
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
n : ℕ
f : L.Functions n
⊢ ClosedUnder.{u, v, w} (M := M) f ∅
have zero : ∀ (f : L.Functions 0), ClosedUnder.{u, v, w} (M := M) f ∅
Tactic: cases n
Cleared hypotheses: n, f
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
n : ℕ
f : L.Functions n
zero : ∀ (f : L.Functions 0), ClosedUnder.{u, v, w} (M := M) f ∅
⊢ ClosedUnder.{u, v, w} (M := M) f ∅
have succ : ∀ (n : ℕ) (f : L.Functions (n + 1)), ClosedUnder.{u, v, w} (M := M) f ∅
Tactic: cases n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
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 : IsEmpty.{u + 1} L.Constants
x : M
⊢ x ∉ ⊥
have h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) ∅
Tactic: have h : (∅ : Set M) ∈ (closure L).closed := by
    rw [mem_closed_iff]
    intro n f
    cases n
    · exact isEmptyElim f
    · intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx
-- 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 : IsEmpty.{u + 1} L.Constants
x : M
h : Membership.mem (γ := Set (Set M)) (LowerAdjoint.closed (u := SetLike.coe) (closure L)) ∅
⊢ x ∉ ⊥
have rw : x ∉ ∅
Tactic: rw [← closure_empty, ← SetLike.mem_coe, 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
S_1 : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure N
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), Membership.mem (γ := Set M) ((⇑φ : (a : M) → N) ⁻¹' (↑S : Set N)) (x i)
⊢ Membership.mem (γ := Set M) ((⇑φ : (a : M) → N) ⁻¹' (↑S : Set N)) (funMap f x)
have rw : funMap f ((⇑φ : (a : M) → N) ∘ x) ∈ (↑S : Set N)
Tactic: rw [mem_preimage, φ.map_fun]
-- 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_1 : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → N
hx : ∀ (i : Fin n), Membership.mem (γ := Set N) ((⇑φ : (a : M) → N) '' (↑S : Set M)) (x i)
⊢ (φ : (a : M) → N)
      (funMap f fun (i : Fin n) ↦
        Classical.choose (p := fun (x_1 : M) ↦ x_1 ∈ (↑S : Set M) ∧ (φ : (a : M) → N) x_1 = x i) ⋯) =
    funMap f x
have simp : funMap f
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑φ : (a : M) → N) fun (i : Fin n) ↦
      Classical.choose (p := fun (x_1 : M) ↦ x_1 ∈ S ∧ (φ : (a : M) → N) x_1 = x i) sorry) =
  funMap f x
Tactic: simp only [Hom.map_fun, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize v xs ↔
    φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ xs)
have rw : φ.Realize (M := M) ((⇑topEquiv : (a : ↥⊤) → M) ∘ v) ((⇑topEquiv : (a : ↥⊤) → M) ∘ xs) ↔
  φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ xs)
Tactic: rw [← StrongHomClass.realize_boundedFormula Substructure.topEquiv φ]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize v ↔ φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)
have rw : φ.Realize (M := M) ((⇑topEquiv : (a : ↥⊤) → M) ∘ v) ↔
  φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)
Tactic: rw [← StrongHomClass.realize_formula Substructure.topEquiv φ]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
p : (x : M) → Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun :
  ∀ {n : ℕ} (f : L.Functions n),
    ClosedUnder.{u, v, w} (M := M) f
      {x : M |
        ∃ (hx : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x), p x hx}
x : M
hx : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x
⊢ p x hx
have refine : ∃ (x_1 : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x), p x x_1
Tactic: refine Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
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_1 : L.Substructure M
L' : Language
inst_3 : L'.Structure M
φ : L →ᴸ L'
inst_4 : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ (↑S : Set M)
⊢ funMap f x ∈ (↑S : Set M)
have h : funMap (φ.onFunction f) x ∈ (↑S : Set M)
Tactic: have h := S.fun_mem (φ.onFunction f) x hx
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (hypothesis)
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_1 : L.Substructure M
L' : Language
inst_3 : L'.Structure M
φ : L →ᴸ L'
inst_4 : φ.IsExpansionOn M
S : L'.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ (↑S : Set M)
h : funMap (φ.onFunction f) x ∈ (↑S : Set M)
⊢ funMap f x ∈ (↑S : Set M)
have h₁ : funMap f x ∈ S
Tactic: simp only [LHom.map_onFunction, Substructure.mem_carrier] at h
Cleared hypotheses: 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
S_1 S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
n : ℕ
f : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n
⊢ ClosedUnder f (↑S : Set M)
have inl : ∀ (f : L.Functions n),
  ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inl f) (↑S : Set M)
Tactic: obtain f | f := f
Cleared hypotheses: f
-- 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_1 S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
n : ℕ
f : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n
inl :
  ∀ (f : L.Functions n),
    ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inl f) (↑S : Set M)
⊢ ClosedUnder f (↑S : Set M)
have inr : ∀ (f : (constantsOn (↑A : Type w)).Functions n),
  ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inr f) (↑S : Set M)
Tactic: obtain f | f := f
Cleared hypotheses: f
-- 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_1 S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
n : ℕ
f : (constantsOn (↑A : Type w)).Functions n
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inr f) (↑S : Set M)
have inr : ∀ (f : (constantsOn (↑A : Type w)).Functions 0),
  ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := 0) (Sum.inr f) (↑S : Set M)
Tactic: cases n
Cleared hypotheses: n, f
-- 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_1 S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
n : ℕ
f : (constantsOn (↑A : Type w)).Functions n
inr :
  ∀ (f : (constantsOn (↑A : Type w)).Functions 0),
    ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := 0) (Sum.inr f) (↑S : Set M)
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inr f) (↑S : Set M)
have inr₁ : ∀ (n : ℕ) (f : (constantsOn (↑A : Type w)).Functions (n + 1)),
  ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n + 1) (Sum.inr f) (↑S : Set M)
Tactic: cases n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
⊢ (LHom.substructureReduct (L.lhomWithConstants (↑A : Type w)) :
        (a : L[[(↑A : Type w)]].Substructure M) → L.Substructure M)
      (S.withConstants (A := A) h) =
    S
have h₁ : ∀ (x : M),
  Membership.mem (γ := L.Substructure M)
      ((LHom.substructureReduct (L.lhomWithConstants (↑A : Type w)) :
            (a : L[[(↑A : Type w)]].Substructure M) → L.Substructure M)
          (S.withConstants (A := A) h) :
        L.Substructure M)
      x ↔
    x ∈ S
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
⊢ Eq (α := (Language.withConstants.{u, v, w} L (↑A : Type w)).Substructure M)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s)
    (withConstants (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (A ∪ s)) (A := A) ⋯)
have refine : LE.le (α := (Language.withConstants.{u, v, w} L (↑A : Type w)).Substructure M)
  (withConstants (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (A ∪ s)) (A := A) sorry)
  (LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s)
Tactic: refine closure_eq_of_le ((A.subset_union_right).trans subset_closure) ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
⊢ LE.le (α := L.Substructure M)
    ((LHom.substructureReduct (L.lhomWithConstants (↑A : Type w)) :
          (a : L[[(↑A : Type w)]].Substructure M) → L.Substructure M)
        (withConstants (LowerAdjoint.toFun (u := SetLike.coe) (closure L) (A ∪ s)) (A := A) ⋯) :
      L.Substructure M)
    ((LHom.substructureReduct (L.lhomWithConstants (↑A : Type w)) :
          (a : L[[(↑A : Type w)]].Substructure M) → L.Substructure M)
        (LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s) :
      L.Substructure M)
have simp : A ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s) : Set M)
Tactic: simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct,
    Set.union_subset_iff, and_true]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
⊢ f.range = Substructure.map f ⊤
have h : ∀ (x : N), x ∈ f.range ↔ x ∈ Substructure.map f ⊤
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₁ : Set.range.{u_1, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
  Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  Set.range.{u_1, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₂ : Eq.{u_1 + 1} (α := Set N) (Set.range.{u_1, w + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
  Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
rw : (↑f.range : Set N) = (↑⊤ : Set N) ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₁ :
  Set.range.{u_1, w + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw₂ :
  Eq.{u_1 + 1} (α := Set N) (Set.range.{u_1, w + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
    Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.range = ⊤ ↔ Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have rw₃ : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ↔
  Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
p : L.Substructure N
⊢ f.range ≤ p ↔ comap f p = ⊤
have rw : Substructure.map f ⊤ ≤ p ↔ comap f p = ⊤
Tactic: rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
p : L.Substructure N
rw : Substructure.map f ⊤ ≤ p ↔ comap f p = ⊤
⊢ f.range ≤ p ↔ comap f p = ⊤
have rw₁ : ⊤ ≤ comap f p ↔ comap f p = ⊤
Tactic: rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Substructures (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
p : L.Substructure N
rw : Substructure.map f ⊤ ≤ p ↔ comap f p = ⊤
rw₁ : ⊤ ≤ comap f p ↔ comap f p = ⊤
⊢ f.range ≤ p ↔ comap f p = ⊤
have rw₂ : ⊤ ≤ comap f p ↔ ⊤ ≤ comap f p
Tactic: rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
-- 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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    Membership.mem (γ := Set M) {x : M | Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
      (x i)
⊢ Eq.{u_1 + 1} (α := Fin n → N) ((⇑f : (a : M) → N) ∘ x) ((⇑g : (a : M) → N) ∘ x)
have h : ∀ (x_1 : Fin n), Eq.{u_1 + 1} (α := N) (((⇑f : (a : M) → N) ∘ x) x_1) (((⇑g : (a : M) → N) ∘ x) x_1)
Tactic: ext
-- 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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    Membership.mem (γ := Set M) {x : M | Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
      (x i)
x_1 : Fin n
⊢ Eq.{u_1 + 1} (α := N) (((⇑f : (a : M) → N) ∘ x) x_1) (((⇑g : (a : M) → N) ∘ x) x_1)
have h : Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) (((⇑g : (a : M) → N) ∘ x) x_1 : N)
Tactic: rw [Function.comp_apply]
-- 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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    Membership.mem (γ := Set M) {x : M | Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
      (x i)
x_1 : Fin n
⊢ Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) (((⇑g : (a : M) → N) ∘ x) x_1 : N)
have h : Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) ((g : (a : M) → N) (x x_1) : N)
Tactic: rw [Function.comp_apply]
-- 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
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx :
  ∀ (i : Fin n),
    Membership.mem (γ := Set M) {x : M | Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)}
      (x i)
x_1 : Fin n
⊢ Eq.{u_1 + 1} (α := N) (((⇑f : (a : M) → N) ∘ x) x_1) (((⇑g : (a : M) → N) ∘ x) x_1)
have h : Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) (x x_1) : N) ((g : (a : M) → N) (x x_1) : N)
Tactic: repeat' rw [Function.comp_apply]