awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
rw :
  φ.Realize (M := M) ((⇑topEquiv : (a : ↥⊤) → M) ∘ v) ↔
    φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)
⊢ φ.Realize v ↔ φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)

Tactic:
rw [← StrongHomClass.realize_formula Substructure.topEquiv φ]

Premises used: FirstOrder.Language.StrongHomClass.realize_formula, FirstOrder.Language.Substructure.topEquiv
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize (M := M) ((⇑topEquiv : (a : ↥⊤) → M) ∘ v) ↔
    φ.Realize (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) ∘ v)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
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

Tactic:
Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc

Premises used: Exists.elim
-- Module: Mathlib.ModelTheory.Substructures
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
refine :
  ∃ (x_1 : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x), p x x_1
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc

Premises used: Exists.elim
-- Module: Mathlib.ModelTheory.Substructures
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
⊢ ∃ (x_1 : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x), p x x_1

Tactic:
closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun

Premises used: FirstOrder.Language.Substructure.closure_induction
-- Module: Mathlib.ModelTheory.Substructures
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
⊢ ∃ (x_1 : Membership.mem (γ := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) x), p x x_1

Tactic:
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun
-- Module: Mathlib.ModelTheory.Substructures
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 (φ.onFunction f) x ∈ (↑S : Set M)

Tactic:
have h := S.fun_mem (φ.onFunction f) x hx
-- Module: Mathlib.ModelTheory.Substructures
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

Tactic:
simp only [LHom.map_onFunction, Substructure.mem_carrier] at h

Premises used: FirstOrder.Language.LHom.map_onFunction, FirstOrder.Language.Substructure.mem_carrier
-- Module: Mathlib.ModelTheory.Substructures
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 f x ∈ S
⊢ funMap f x ∈ (↑S : Set M)

Tactic:
h
-- Module: Mathlib.ModelTheory.Substructures
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 f x ∈ S
⊢ funMap f x ∈ (↑S : Set M)

Tactic:
exact h
-- Module: Mathlib.ModelTheory.Substructures
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 T : L'.Substructure M
h :
  Eq.{w + 1} (α := L.Substructure M)
    ((fun (S : L'.Substructure M) ↦ ({ carrier := (↑S : Set M), fun_mem := ⋯ } : L.Substructure M)) S)
    ((fun (S : L'.Substructure M) ↦ ({ carrier := (↑S : Set M), fun_mem := ⋯ } : L.Substructure M)) T)
⊢ S = T

Tactic:
simp only [SetLike.coe_set_eq, Substructure.mk.injEq] at h

Premises used: FirstOrder.Language.Substructure.mk.injEq, SetLike.coe_set_eq
-- Module: Mathlib.ModelTheory.Substructures
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 T : L'.Substructure M
h : S = T
⊢ S = T

Tactic:
h
-- Module: Mathlib.ModelTheory.Substructures
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 T : L'.Substructure M
h : S = T
⊢ S = T

Tactic:
exact h
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
x : M
S : L'.Substructure M
⊢ Membership.mem (γ := L.Substructure M)
      ((φ.substructureReduct : (a : L'.Substructure M) → L.Substructure M) S : L.Substructure M) x ↔
    x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
S : L'.Substructure M
⊢ (↑((φ.substructureReduct : (a : L'.Substructure M) → L.Substructure M) S : L.Substructure M) : Set M) = (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
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)
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)
⊢ ClosedUnder f (↑S : Set M)

Tactic:
obtain f | f := f
-- Module: Mathlib.ModelTheory.Substructures
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 : L.Functions n
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inl f) (↑S : Set M)

Tactic:
S.fun_mem f

Premises used: Set.Mem, FirstOrder.Language.Substructure.fun_mem, FirstOrder.Language.ClosedUnder, Sum.elim
-- Module: Mathlib.ModelTheory.Substructures
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 : L.Functions n
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inl f) (↑S : Set M)

Tactic:
exact S.fun_mem f

Premises used: FirstOrder.Language.Substructure.fun_mem
-- Module: Mathlib.ModelTheory.Substructures
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)
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)
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n) (Sum.inr f) (↑S : Set M)

Tactic:
cases n
-- Module: Mathlib.ModelTheory.Substructures
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)
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:
fun _ _ => h f.2

Premises used: FirstOrder.Language.ClosedUnder, Subtype.property
-- Module: Mathlib.ModelTheory.Substructures
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)
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:
exact fun _ _ => h f.2

Premises used: Subtype.property
-- Module: Mathlib.ModelTheory.Substructures
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 + 1)
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n + 1) (Sum.inr f) (↑S : Set M)

Tactic:
isEmptyElim f

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.Substructures
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 + 1)
⊢ ClosedUnder (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (n := n + 1) (Sum.inr f) (↑S : Set M)

Tactic:
exact isEmptyElim f
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
x : M
⊢ x ∈ S.withConstants (A := A) h ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
⊢ (↑(S.withConstants (A := A) h) : Set M) = (↑S : Set M)

Tactic:
rfl

Premises used: FirstOrder.Language.withConstants, FirstOrder.Language.sum, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
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
⊢ (LHom.substructureReduct (L.lhomWithConstants (↑A : Type w)) :
        (a : L[[(↑A : Type w)]].Substructure M) → L.Substructure M)
      (S.withConstants (A := A) h) =
    S

Tactic:
ext
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ (↑S : Set M)
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:
simp
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
a : M
ha : a ∈ A
a' : (Language.withConstants.{u, v, w} L (↑A : Type w)).Constants :=
  Sum.inr (Subtype.mk (p := fun (x : M) ↦ x ∈ A) a ha)
⊢ Membership.mem (γ := (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) a

Tactic:
constants_mem a'

Premises used: Set.Mem, FirstOrder.Language.Substructure.constants_mem, FirstOrder.Language.constantMap, Sum.elim
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
a : M
ha : a ∈ A
a' : (Language.withConstants.{u, v, w} L (↑A : Type w)).Constants :=
  Sum.inr (Subtype.mk (p := fun (x : M) ↦ x ∈ A) a ha)
⊢ Membership.mem (γ := (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) a

Tactic:
exact constants_mem a'

Premises used: FirstOrder.Language.Substructure.constants_mem
-- Module: Mathlib.ModelTheory.Substructures
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) ⋯)

Tactic:
closure_eq_of_le ((A.subset_union_right).trans subset_closure) ?_

Premises used: Set.Mem, setOf, Set.subset_union_right, HasSubset.Subset.trans, FirstOrder.Language.Substructure.closure_eq_of_le, FirstOrder.Language.Substructure.subset_closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
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) ⋯)
    (LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s)
⊢ 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) ⋯)

Tactic:
refine closure_eq_of_le ((A.subset_union_right).trans subset_closure) ?_

Premises used: Set.subset_union_right, HasSubset.Subset.trans, FirstOrder.Language.Substructure.closure_eq_of_le, FirstOrder.Language.Substructure.subset_closure
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
simp :
  A ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) 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)

Tactic:
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct,
    Set.union_subset_iff, and_true]

Premises used: and_true, Set.union_subset_iff, FirstOrder.Language.LHom.coe_substructureReduct, FirstOrder.Language.Substructure.reduct_withConstants, FirstOrder.Language.Substructure.subset_closure, FirstOrder.Language.Substructure.closure_le
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
⊢ A ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s) : Set M)

Tactic:
subset_closure_withConstants

Premises used: Set.Mem, setOf, FirstOrder.Language.Substructure.subset_closure_withConstants
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
A s : Set M
⊢ A ⊆ (↑(LowerAdjoint.toFun (u := SetLike.coe) (closure (Language.withConstants.{u, v, w} L (↑A : Type w))) s) : Set M)

Tactic:
exact subset_closure_withConstants

Premises used: FirstOrder.Language.Substructure.subset_closure_withConstants
-- Module: Mathlib.ModelTheory.Substructures
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
p : L.Substructure N
f_1 : M →[L] N
h : ∀ (c : M), Membership.mem (α := N) p ((f_1 : (a : M) → N) c : N)
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{u_1 + 1} (α := ↥p) (Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f_1 : (a : M) → N) (funMap f x)) ⋯ : ↥p)
    (funMap f ((fun (c : M) ↦ Subtype.mk (p := fun (x : N) ↦ x ∈ p) ((f_1 : (a : M) → N) c) ⋯) ∘ x) : ↥p)

Tactic:
aesop
-- Module: Mathlib.ModelTheory.Substructures
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
f : M →[L] N
g : N →[L] P
p : L.Substructure P
h : ∀ (b : N), Membership.mem (α := P) p ((g : (a : N) → P) b : P)
⊢ (codRestrict p g h).comp f = codRestrict p (g.comp f) ⋯

Tactic:
ext fun _ => rfl

Premises used: FirstOrder.Language.Hom.ext, rfl
-- Module: Mathlib.ModelTheory.Substructures
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
h : ∀ (b : M), Membership.mem (α := N) p ((f : (a : M) → N) b : N)
⊢ p.subtype.toHom.comp (codRestrict p f h) = f

Tactic:
ext fun _ => rfl

Premises used: FirstOrder.Language.Hom.ext, rfl
-- Module: Mathlib.ModelTheory.Substructures
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
g : N →[L] P
f : M →[L] N
p : L.Substructure N
h : ∀ (b : M), Membership.mem (α := N) p ((f : (a : M) → N) b : N)
⊢ (g.domRestrict p).comp (codRestrict p f h) = g.comp f

Tactic:
rfl

Premises used: FirstOrder.Language.Hom.comp, FirstOrder.Language.Hom.domRestrict, rfl
-- Module: Mathlib.ModelTheory.Substructures
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 : Set N) = Set.range.{u_1, w + 1} (ι := M) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
x : N
⊢ x ∈ f.range ↔ ∃ (y : M), (f : (a : M) → N) y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
h : ∀ (x : N), x ∈ f.range ↔ x ∈ Substructure.map f ⊤
⊢ f.range = Substructure.map f ⊤

Tactic:
ext
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
x : N
⊢ x ∈ f.range ↔ x ∈ Substructure.map f ⊤

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
x : M
⊢ Membership.mem (α := N) f.range ((f : (a : M) → N) x : N)

Tactic:
⟨x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Eq (α := L.Substructure M) (range (id L M)) ⊤

Tactic:
SetLike.coe_injective Set.range_id

Premises used: SetLike.coe_injective, Set.range_id
-- Module: Mathlib.ModelTheory.Substructures
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
f : M →[L] N
g : N →[L] P
⊢ (g.comp f).range = Substructure.map g f.range

Tactic:
SetLike.coe_injective (Set.range_comp g f)

Premises used: Set.range_comp, SetLike.coe_injective, DFunLike.coe
-- Module: Mathlib.ModelTheory.Substructures
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
f : M →[L] N
g : N →[L] P
⊢ (g.comp f).range ≤ g.range

Tactic:
SetLike.coe_mono (Set.range_comp_subset_range f g)

Premises used: Set.range_comp_subset_range, Set.Subset, DFunLike.coe, SetLike.coe_mono
-- Module: Mathlib.ModelTheory.Substructures
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)
rw₃ 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)
⊢ f.range = ⊤ ↔ 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]

Premises used: Set.range_eq_univ, FirstOrder.Language.Substructure.coe_top, SetLike.ext'_iff, FirstOrder.Language.Hom.range_coe
-- Module: Mathlib.ModelTheory.Substructures
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 = ⊤
rw₂ rw₃ : ⊤ ≤ comap f p ↔ ⊤ ≤ comap f p
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

Premises used: eq_top_iff, FirstOrder.Language.Hom.range_eq_map, FirstOrder.Language.Substructure.map_le_iff_le_comap
-- Module: Mathlib.ModelTheory.Substructures
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 M
⊢ Substructure.map f p ≤ f.range

Tactic:
SetLike.coe_mono (Set.image_subset_range f p)

Premises used: Set.image_subset_range, Set.Subset, SetLike.coe, DFunLike.coe, SetLike.coe_mono