awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 ∉ ∅

Tactic:
Set.notMem_empty _

Premises used: Set.notMem_empty
-- 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
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 ∉ ∅

Tactic:
exact Set.notMem_empty _

Premises used: Set.notMem_empty
-- 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
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)
rw : funMap f ((⇑φ : (a : M) → N) ∘ x) ∈ (↑S : Set N)
⊢ Membership.mem (γ := Set M) ((⇑φ : (a : M) → N) ⁻¹' (↑S : Set N)) (funMap f x)

Tactic:
rw [mem_preimage, φ.map_fun]

Premises used: FirstOrder.Language.Hom.map_fun, Set.mem_preimage
-- 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
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)
⊢ funMap f ((⇑φ : (a : M) → N) ∘ x) ∈ (↑S : Set N)

Tactic:
S.fun_mem f (φ ∘ x) hx

Premises used: Set.Mem, FirstOrder.Language.Substructure.fun_mem, Function.comp, 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
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)
⊢ funMap f ((⇑φ : (a : M) → N) ∘ x) ∈ (↑S : Set N)

Tactic:
exact S.fun_mem f (φ ∘ x) hx

Premises used: FirstOrder.Language.Substructure.fun_mem, Function.comp, DFunLike.coe
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure N
f : M →[L] N
x : M
⊢ x ∈ comap f S ↔ Membership.mem (α := N) S ((f : (a : M) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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 P
g : N →[L] P
f : M →[L] N
⊢ comap f (comap g S) = comap (g.comp f) S

Tactic:
rfl

Premises used: Set.Mem, FirstOrder.Language.Hom.comp, setOf, Set.preimage, FirstOrder.Language.Substructure.comap, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
P : Type u_2
inst : L.Structure P
S : L.Substructure P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S

Tactic:
simp
-- 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
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)
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) ⋯) =
    funMap f x
⊢ (φ : (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

Tactic:
simp only [Hom.map_fun, SetLike.mem_coe]

Premises used: FirstOrder.Language.Hom.map_fun, SetLike.mem_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
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)
⊢ 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) ⋯) =
    funMap f x

Tactic:
congr rfl (funext fun i => (Classical.choose_spec (hx i)).2)

Premises used: Classical.choose_spec, funext, And.right, congr, 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 : 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)
⊢ 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) ⋯) =
    funMap f x

Tactic:
exact congr rfl (funext fun i => (Classical.choose_spec (hx i)).2)

Premises used: Classical.choose_spec, funext, And.right, congr, 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
S : L.Substructure M
y : N
⊢ y ∈ map f S ↔ ∃ x ∈ S, (f : (a : M) → N) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- 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
S : L.Substructure M
x : M
hx : x ∈ S
⊢ Membership.mem (α := N) (map f S) ((f : (a : M) → N) x : N)

Tactic:
mem_image_of_mem f hx

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.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
S : L.Substructure M
x : ↥S
⊢ Membership.mem (α := N) (map f S) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
mem_map_of_mem f x.prop

Premises used: Subtype.prop, FirstOrder.Language.Substructure.mem_map_of_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 : L.Substructure M
g : N →[L] P
f : M →[L] N
⊢ map g (map f S) = map (g.comp f) S

Tactic:
SetLike.coe_injective <| image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- 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
S : L.Substructure M
T : L.Substructure N
⊢ map f S ≤ T ↔ S ≤ comap f T

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- 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
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: FirstOrder.Language.Substructure.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure M
T : L.Substructure N
f : M →[L] N
⊢ S ≤ comap f T → map f S ≤ T

Tactic:
(gc_map_comap f).l_le

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.l_le
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure M
T : L.Substructure N
f : M →[L] N
⊢ map f S ≤ T → S ≤ comap f T

Tactic:
(gc_map_comap f).le_u

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.le_u
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure M
f : M →[L] N
⊢ S ≤ comap f (map f S)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.le_u_l
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure N
f : M →[L] N
⊢ map f (comap f S) ≤ S

Tactic:
(gc_map_comap f).l_u_le _

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.l_u_le
-- 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
⊢ Monotone (map f)

Tactic:
(gc_map_comap f).monotone_l

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.monotone_l
-- 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
⊢ Monotone (comap f)

Tactic:
(gc_map_comap f).monotone_u

Premises used: GaloisConnection.monotone_u, FirstOrder.Language.Substructure.gc_map_comap
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure M
f : M →[L] N
⊢ map f (comap f (map f S)) = map f S

Tactic:
(gc_map_comap f).l_u_l_eq_l _

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.l_u_l_eq_l
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S : L.Substructure N
f : M →[L] N
⊢ comap f (map f (comap f S)) = comap f S

Tactic:
(gc_map_comap f).u_l_u_eq_u _

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S T : L.Substructure M
f : M →[L] N
⊢ map f (S ⊔ T) = map f S ⊔ map f T

Tactic:
(gc_map_comap f).l_sup

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
ι : Sort u_3
f : M →[L] N
s : ι → L.Substructure M
⊢ map f (⨆ (i : ι), s i) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
S T : L.Substructure N
f : M →[L] N
⊢ comap f (S ⊓ T) = comap f S ⊓ comap f T

Tactic:
(gc_map_comap f).u_inf

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
ι : Sort u_3
f : M →[L] N
s : ι → L.Substructure N
⊢ comap f (⨅ (i : ι), s i) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.u_iInf
-- 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
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.l_bot
-- 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
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: FirstOrder.Language.Substructure.gc_map_comap, GaloisConnection.u_top
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ map (Hom.id L M) S = S

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- 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
s : Set M
⊢ map f (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s) =
    LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' s)

Tactic:
Eq.symm <|
    closure_eq_of_le (Set.image_mono subset_closure) <|
      map_le_iff_le_comap.2 <| closure_le.2 fun x hx => subset_closure ⟨x, hx, rfl⟩

Premises used: Iff.mpr, Set.image_mono, FirstOrder.Language.Substructure.closure_eq_of_le, FirstOrder.Language.Substructure.subset_closure, And.intro, Exists.intro, FirstOrder.Language.Substructure.map_le_iff_le_comap, FirstOrder.Language.Substructure.closure_le, Eq.symm, rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
s : Set M
f : M →[L] N
⊢ LowerAdjoint.toFun (u := SetLike.coe) (closure L) ((⇑f : (a : M) → N) '' s) =
    map f (LowerAdjoint.toFun (u := SetLike.coe) (closure L) s)

Tactic:
(map_closure f s).symm

Premises used: FirstOrder.Language.Substructure.map_closure, Eq.symm
-- 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
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : L.Substructure M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
simp [mem_comap, mem_map, hf.eq_iff]

Premises used: Function.Injective.eq_iff, FirstOrder.Language.Substructure.mem_map, FirstOrder.Language.Substructure.mem_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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : L.Substructure M
⊢ comap f (map f S) = S

Tactic:
(gciMapComap hf).u_l_eq _

Premises used: FirstOrder.Language.Substructure.gciMapComap, GaloisCoinsertion.u_l_eq
-- 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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Surjective (comap f)

Tactic:
(gciMapComap hf).u_surjective

Premises used: FirstOrder.Language.Substructure.gciMapComap, GaloisCoinsertion.u_surjective
-- 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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Injective (map f)

Tactic:
(gciMapComap hf).l_injective

Premises used: GaloisCoinsertion.l_injective, FirstOrder.Language.Substructure.gciMapComap
-- 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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : L.Substructure M
⊢ comap f (map f S ⊓ map f T) = S ⊓ T

Tactic:
(gciMapComap hf).u_inf_l _ _

Premises used: FirstOrder.Language.Substructure.gciMapComap, GaloisCoinsertion.u_inf_l
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_3
f : M →[L] N
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → L.Substructure M
⊢ comap f (⨅ (i : ι), map f (S i)) = ⨅ (i : ι), S i

Tactic:
(gciMapComap hf).u_iInf_l _

Premises used: GaloisCoinsertion.u_iInf_l, FirstOrder.Language.Substructure.gciMapComap
-- 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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : L.Substructure M
⊢ comap f (map f S ⊔ map f T) = S ⊔ T

Tactic:
(gciMapComap hf).u_sup_l _ _

Premises used: FirstOrder.Language.Substructure.gciMapComap, GaloisCoinsertion.u_sup_l
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_3
f : M →[L] N
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → L.Substructure M
⊢ comap f (⨆ (i : ι), map f (S i)) = ⨆ (i : ι), S i

Tactic:
(gciMapComap hf).u_iSup_l _

Premises used: FirstOrder.Language.Substructure.gciMapComap, GaloisCoinsertion.u_iSup_l
-- 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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : L.Substructure M
⊢ map f S ≤ map f T ↔ S ≤ T

Tactic:
(gciMapComap hf).l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, FirstOrder.Language.Substructure.gciMapComap
-- 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
hf : Function.Injective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ StrictMono (map f)

Tactic:
(gciMapComap hf).strictMono_l

Premises used: GaloisCoinsertion.strictMono_l, FirstOrder.Language.Substructure.gciMapComap
-- 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
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : L.Substructure N
x : N
h : x ∈ S
y : M
hy : (f : (a : M) → N) y = x
⊢ y ∈ comap f S ∧ (f : (a : M) → N) y = x

Tactic:
simp [hy, h]
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : L.Substructure N
⊢ map f (comap f S) = S

Tactic:
(giMapComap hf).l_u_eq _

Premises used: FirstOrder.Language.Substructure.giMapComap, GaloisInsertion.l_u_eq
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Surjective (map f)

Tactic:
(giMapComap hf).l_surjective

Premises used: FirstOrder.Language.Substructure.giMapComap, GaloisInsertion.l_surjective
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Injective (comap f)

Tactic:
(giMapComap hf).u_injective

Premises used: GaloisInsertion.u_injective, FirstOrder.Language.Substructure.giMapComap
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : L.Substructure N
⊢ map f (comap f S ⊓ comap f T) = S ⊓ T

Tactic:
(giMapComap hf).l_inf_u _ _

Premises used: FirstOrder.Language.Substructure.giMapComap, GaloisInsertion.l_inf_u
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_3
f : M →[L] N
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → L.Substructure N
⊢ map f (⨅ (i : ι), comap f (S i)) = ⨅ (i : ι), S i

Tactic:
(giMapComap hf).l_iInf_u _

Premises used: GaloisInsertion.l_iInf_u, FirstOrder.Language.Substructure.giMapComap
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : L.Substructure N
⊢ map f (comap f S ⊔ comap f T) = S ⊔ T

Tactic:
(giMapComap hf).l_sup_u _ _

Premises used: GaloisInsertion.l_sup_u, FirstOrder.Language.Substructure.giMapComap
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_3
f : M →[L] N
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → L.Substructure N
⊢ map f (⨆ (i : ι), comap f (S i)) = ⨆ (i : ι), S i

Tactic:
(giMapComap hf).l_iSup_u _

Premises used: FirstOrder.Language.Substructure.giMapComap, GaloisInsertion.l_iSup_u
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : L.Substructure N
⊢ comap f S ≤ comap f T ↔ S ≤ T

Tactic:
(giMapComap hf).u_le_u_iff

Premises used: FirstOrder.Language.Substructure.giMapComap, GaloisInsertion.u_le_u_iff
-- 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
hf : Function.Surjective.{w + 1, u_1 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ StrictMono (comap f)

Tactic:
(giMapComap hf).strictMono_u

Premises used: GaloisInsertion.strictMono_u, FirstOrder.Language.Substructure.giMapComap
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
x : ↥S
⊢ (S.subtype : (a : ↥S) → M) x = (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ Function.Injective (α := ↥S) (β := M) (⇑S.subtype : (a : ↥S) → M)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
S : L.Substructure M
⊢ Eq (α := (a : ↥S) → M) (⇑S.subtype : (a : ↥S) → M) (Subtype.val (p := fun (x : M) ↦ x ∈ S))

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 : L.Substructure M
s : Set M
m : ↥⊤
⊢ (fun (m : M) ↦ (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x) m ⋯ : ↥⊤))
      ((subtype ⊤ : (a : ↥⊤) → M) m) =
    m

Tactic:
simp
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ Eq.{w + 1} (α := (a : ↥⊤) → M) (⇑topEquiv : (a : ↥⊤) → M)
    (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := L.Substructure M) ⊤ x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
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)
⊢ φ.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)

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

Premises used: FirstOrder.Language.StrongHomClass.realize_boundedFormula, FirstOrder.Language.Substructure.topEquiv
-- Module: Mathlib.ModelTheory.Substructures
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.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:
simp