[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
p q : Substructure L M
h : ↑p = ↑q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
q : Substructure L M
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝, fun_mem := fun_mem✝ } = ↑q
⊢ { carrier := carrier✝, fun_mem := fun_mem✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
carrier✝¹ : Set M
fun_mem✝¹ : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f carrier✝¹
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = ↑{ carrier := carrier✝, fun_mem := fun_mem✝ }
⊢ { carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = { carrier := carrier✝, fun_mem := fun_mem✝ }
[PROOFSTEP]
congr
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_3
t : Term L α
xs : α → M
h : ∀ (a : α), xs a ∈ S
⊢ realize xs t ∈ S
[PROOFSTEP]
induction' t with a n f ts ih
[GOAL]
case var
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S
[PROOFSTEP]
exact h a
[GOAL]
case func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih : ∀ (a : Fin n), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S
[PROOFSTEP]
exact Substructure.fun_mem _ _ _ ih
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
⊢ ∀ (s_1 : Set M), (s_1 ∈ Set.range fun t => ⋂ (_ : t ∈ s), ↑t) → ClosedUnder f s_1
[PROOFSTEP]
rintro _ ⟨t, rfl⟩
[GOAL]
case intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
t : Substructure L M
⊢ ClosedUnder f ((fun t => ⋂ (_ : t ∈ s), ↑t) t)
[PROOFSTEP]
by_cases h : t ∈ s
[GOAL]
case pos
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
t : Substructure L M
h : t ∈ s
⊢ ClosedUnder f ((fun t => ⋂ (_ : t ∈ s), ↑t) t)
[PROOFSTEP]
simpa [h] using t.fun_mem f
[GOAL]
case neg
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
t : Substructure L M
h : ¬t ∈ s
⊢ ClosedUnder f ((fun t => ⋂ (_ : t ∈ s), ↑t) t)
[PROOFSTEP]
simp [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
ι : Sort u_3
S : ι → Substructure L M
x : M
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
ι : Sort u_3
S : ι → Substructure L M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
[PROOFSTEP]
let S : L.Substructure M :=
  ⟨range (Term.realize (L := L) ((↑) : s → M)), fun {n} f x hx =>
    by
    simp only [mem_range] at *
    refine' ⟨func f fun i => Classical.choose (hx i), _⟩
    simp only [Term.realize, fun i => Classical.choose_spec (hx i)]⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)
⊢ funMap f x ∈ range (Term.realize Subtype.val)
[PROOFSTEP]
simp only [mem_range] at *
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ ∃ y, Term.realize Subtype.val y = funMap f x
[PROOFSTEP]
refine' ⟨func f fun i => Classical.choose (hx i), _⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ Term.realize Subtype.val (func f fun i => Classical.choose (_ : ∃ y, Term.realize Subtype.val y = x i)) = funMap f x
[PROOFSTEP]
simp only [Term.realize, fun i => Classical.choose_spec (hx i)]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
[PROOFSTEP]
change _ = (S : Set M)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = ↑S
[PROOFSTEP]
rw [← SetLike.ext'_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ LowerAdjoint.toFun (closure L) s = S
[PROOFSTEP]
refine' closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => _)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'
[PROOFSTEP]
rintro _ ⟨t, rfl⟩
[GOAL]
case intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
t : Term L { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'
[PROOFSTEP]
exact t.realize_mem _ fun i => hS' i.2
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Small.{u, w} ↑s
⊢ Small.{u, w} { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
rw [← SetLike.coe_sort_coe, Substructure.coe_closure_eq_range_term_realize]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Small.{u, w} ↑s
⊢ Small.{u, w} ↑(range (Term.realize Subtype.val))
[PROOFSTEP]
exact small_range _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
x : M
⊢ x ∈ LowerAdjoint.toFun (closure L) s ↔ ∃ t, Term.realize Subtype.val t = x
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ #(Term L ↑s)
[PROOFSTEP]
rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #↑(range (Term.realize Subtype.val)) ≤ #(Term L ↑s)
[PROOFSTEP]
rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #↑(range (Term.realize Subtype.val)) ≤ lift #(Term L ↑s)
[PROOFSTEP]
exact Cardinal.mk_range_le_lift
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ max ℵ₀ (lift #↑s + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
rw [← lift_umax]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ max ℵ₀ (lift #↑s + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
refine' lift_card_closure_le_card_term.trans (Term.card_le.trans _)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ max ℵ₀ #(↑s ⊕ (i : ℕ) × Functions L i) ≤ max ℵ₀ (lift #↑s + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
rw [mk_sum, lift_umax.{w, u}]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
haveI : Countable s := h.to_subtype
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ ℵ₀
[PROOFSTEP]
exact lift_card_closure_le_card_term.trans mk_le_aleph0
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
⊢ p x
[PROOFSTEP]
have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
this : ∀ (x : M), x ∈ LowerAdjoint.toFun (closure L) s → p x
⊢ p x
[PROOFSTEP]
simpa [hs] using this x
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ Small.{u, w} { x // x ∈ ⊥ }
[PROOFSTEP]
rw [← closure_empty]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ Small.{u, w} { x // x ∈ LowerAdjoint.toFun (closure L) ∅ }
[PROOFSTEP]
haveI : Small.{u} (∅ : Set M) := small_subsingleton _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
this : Small.{u, w} ↑∅
⊢ Small.{u, w} { x // x ∈ LowerAdjoint.toFun (closure L) ∅ }
[PROOFSTEP]
exact Substructure.small_closure
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L N
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑φ ⁻¹' ↑S
⊢ funMap f x ∈ ↑φ ⁻¹' ↑S
[PROOFSTEP]
rw [mem_preimage, φ.map_fun]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L N
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑φ ⁻¹' ↑S
⊢ funMap f (↑φ ∘ x) ∈ ↑S
[PROOFSTEP]
exact S.fun_mem f (φ ∘ x) hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L M
n : ℕ
f : Functions L n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ↑φ '' ↑S
⊢ (fun a => ↑φ a) (funMap f fun i => Classical.choose (_ : x i ∈ ↑φ '' ↑S)) = funMap f x
[PROOFSTEP]
simp only [Hom.map_fun, SetLike.mem_coe]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L M
n : ℕ
f : Functions L n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ↑φ '' ↑S
⊢ funMap f (↑φ ∘ fun i => Classical.choose (_ : ∃ x_1, (fun x_2 => x_2 ∈ S ∧ ↑φ x_2 = x i) x_1)) = funMap f x
[PROOFSTEP]
exact congr rfl (funext fun i => (Classical.choose_spec (hx i)).2)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Injective ↑f
S : Substructure L M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S
[PROOFSTEP]
simp [mem_comap, mem_map, hf.eq_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Surjective ↑f
S : Substructure L N
x : N
h : x ∈ S
y : M
hy : ↑f y = x
⊢ y ∈ comap f S ∧ ↑f y = x
[PROOFSTEP]
simp [hy, h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
m : { x // x ∈ ⊤ }
⊢ (fun m => { val := m, property := (_ : m ∈ ⊤) }) (↑(subtype ⊤) m) = m
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ p x hx
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ closure L s) (hc : p x hx) => hc
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ ∃ x_1, p x x_1
[PROOFSTEP]
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S : Substructure L' M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
⊢ funMap f x ∈ ↑S
[PROOFSTEP]
have h := S.fun_mem (φ.onFunction f) x hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S : Substructure L' M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap (onFunction φ f) x ∈ ↑S
⊢ funMap f x ∈ ↑S
[PROOFSTEP]
simp only [LHom.map_onFunction, Substructure.mem_carrier] at h 
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S : Substructure L' M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap f x ∈ S
⊢ funMap f x ∈ ↑S
[PROOFSTEP]
exact h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S T : Substructure L' M
h :
  (fun S =>
        { carrier := ↑S,
          fun_mem := (_ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), (∀ (i : Fin n), x i ∈ ↑S) → funMap f x ∈ S) })
      S =
    (fun S =>
        { carrier := ↑S,
          fun_mem := (_ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), (∀ (i : Fin n), x i ∈ ↑S) → funMap f x ∈ S) })
      T
⊢ S = T
[PROOFSTEP]
simp only [SetLike.coe_set_eq, Substructure.mk.injEq] at h 
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S T : Substructure L' M
h : S = T
⊢ S = T
[PROOFSTEP]
exact h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : Functions (L[[↑A]]) n
⊢ ClosedUnder f ↑S
[PROOFSTEP]
cases' f with f f
[GOAL]
case inl
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : Functions L n
⊢ ClosedUnder (Sum.inl f) ↑S
[PROOFSTEP]
exact S.fun_mem f
[GOAL]
case inr
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : Functions (constantsOn ↑A) n
⊢ ClosedUnder (Sum.inr f) ↑S
[PROOFSTEP]
cases n
[GOAL]
case inr.zero
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
f : Functions (constantsOn ↑A) Nat.zero
⊢ ClosedUnder (Sum.inr f) ↑S
[PROOFSTEP]
exact fun _ _ => h f.2
[GOAL]
case inr.succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n✝ : ℕ
f : Functions (constantsOn ↑A) (Nat.succ n✝)
⊢ ClosedUnder (Sum.inr f) ↑S
[PROOFSTEP]
exact isEmptyElim f
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) = S
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) ↔ x✝ ∈ S
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
intro a ha
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
simp only [SetLike.mem_coe]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
[PROOFSTEP]
let a' : L[[A]].Constants := Sum.inr ⟨a, ha⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
a' : Language.Constants (L[[↑A]]) := Sum.inr { val := a, property := ha }
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
[PROOFSTEP]
exact constants_mem a'
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ LowerAdjoint.toFun (closure (L[[↑A]])) s =
    withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))
[PROOFSTEP]
refine' closure_eq_of_le ((A.subset_union_right s).trans subset_closure) _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s))) ≤
    LowerAdjoint.toFun (closure (L[[↑A]])) s
[PROOFSTEP]
rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A))
      (withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))) ≤
    ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct, Set.union_subset_iff,
  and_true_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
exact subset_closure_withConstants
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f✝ : M →[L] N
h : ∀ (c : M), ↑f✝ c ∈ p
n : ℕ
f : Functions L n
x : Fin n → M
⊢ (fun c => { val := ↑f✝ c, property := (_ : ↑f✝ c ∈ p) }) (funMap f x) =
    funMap f ((fun c => { val := ↑f✝ c, property := (_ : ↑f✝ c ∈ p) }) ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
⊢ range f = Substructure.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
x✝ : N
⊢ x✝ ∈ range f ↔ x✝ ∈ Substructure.map f ⊤
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
⊢ range f = ⊤ ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_iff_surjective]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
p : Substructure L N
⊢ range f ≤ p ↔ comap f p = ⊤
[PROOFSTEP]
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
⊢ funMap fn x ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
have h : f ∘ x = g ∘ x := by
  ext
  repeat' rw [Function.comp_apply]
  apply hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
⊢ ↑f ∘ x = ↑g ∘ x
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ (↑f ∘ x) x✝ = (↑g ∘ x) x✝
[PROOFSTEP]
repeat' rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ (↑f ∘ x) x✝ = (↑g ∘ x) x✝
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ ↑f (x x✝) = (↑g ∘ x) x✝
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ ↑f (x x✝) = ↑g (x x✝)
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ ↑f (x x✝) = ↑g (x x✝)
[PROOFSTEP]
apply hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
h : ↑f ∘ x = ↑g ∘ x
⊢ funMap fn x ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
simp [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r
      ({ toFun := ↑(Hom.codRestrict p (toHom f) h),
            inj' :=
              (_ :
                ∀ (a b : M), ↑(Hom.codRestrict p (toHom f) h) a = ↑(Hom.codRestrict p (toHom f) h) b → a = b) }.toFun ∘
        x) ↔
    RelMap r x
[PROOFSTEP]
simp only
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(Hom.codRestrict p (toHom f) h) ∘ x) ↔ RelMap r x
[PROOFSTEP]
rw [← p.subtype.map_rel]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(subtype p) ∘ ↑(Hom.codRestrict p (toHom f) h) ∘ x) ↔ RelMap r x
[PROOFSTEP]
change RelMap r (Hom.comp p.subtype.toHom (f.toHom.codRestrict p h) ∘ x) ↔ _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(Hom.comp (toHom (subtype p)) (Hom.codRestrict p (toHom f) h)) ∘ x) ↔ RelMap r x
[PROOFSTEP]
rw [Hom.subtype_comp_codRestrict, ← f.map_rel]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(toHom f) ∘ x) ↔ RelMap r (↑f ∘ x)
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f✝ : M ↪[L] N
s : Substructure L M
n : ℕ
f : Functions L n
x : Fin n → { x // x ∈ s }
⊢ Equiv.toFun
      {
        toFun :=
          ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
              (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s)),
        invFun := fun n =>
          { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
            property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) },
        left_inv :=
          (_ :
            ∀ (x : { x // x ∈ s }),
              (fun n =>
                    { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                      property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                  (↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                        (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : { x // x ∈ Substructure.map (toHom f✝) s }),
              ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                      (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                  ((fun n =>
                      { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                        property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                    x) =
                x) }
      (funMap f x) =
    funMap f
      ({
            toFun :=
              ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                  (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s)),
            invFun := fun n =>
              { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) },
            left_inv :=
              (_ :
                ∀ (x : { x // x ∈ s }),
                  (fun n =>
                        { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                          property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                      (↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                            (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Substructure.map (toHom f✝) s }),
                  ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                          (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                      ((fun n =>
                          { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                            property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                        x) =
                    x) }.toFun ∘
        x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ↪[L] N
s : Substructure L M
n : ℕ
R : Relations L n
x : Fin n → { x // x ∈ s }
⊢ RelMap R
      ({
            toFun :=
              ↑(codRestrict (Substructure.map (toHom f) s) (domRestrict f s)
                  (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f s) x ∈ Substructure.map (toHom f) s)),
            invFun := fun n =>
              { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s),
                property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s) ∈ ↑s) },
            left_inv :=
              (_ :
                ∀ (x : { x // x ∈ s }),
                  (fun n =>
                        { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s),
                          property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s) ∈ ↑s) })
                      (↑(codRestrict (Substructure.map (toHom f) s) (domRestrict f s)
                            (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f s) x ∈ Substructure.map (toHom f) s))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Substructure.map (toHom f) s }),
                  ↑(codRestrict (Substructure.map (toHom f) s) (domRestrict f s)
                          (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f s) x ∈ Substructure.map (toHom f) s))
                      ((fun n =>
                          { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s),
                            property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s) ∈ ↑s) })
                        x) =
                    x) }.toFun ∘
        x) ↔
    RelMap R x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f✝ : M ↪[L] N
n : ℕ
f : Functions L n
x : Fin n → M
⊢ Equiv.toFun
      { toFun := ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝))),
        invFun := fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)),
        left_inv :=
          (_ :
            ∀ (m : M),
              (fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)))
                  (↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝))) m) =
                m),
        right_inv :=
          (_ :
            ∀ (x : { x // x ∈ Hom.range (toHom f✝) }),
              ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝)))
                  ((fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝))) x) =
                x) }
      (funMap f x) =
    funMap f
      ({ toFun := ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝))),
            invFun := fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)),
            left_inv :=
              (_ :
                ∀ (m : M),
                  (fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)))
                      (↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝)))
                        m) =
                    m),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Hom.range (toHom f✝) }),
                  ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝)))
                      ((fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝))) x) =
                    x) }.toFun ∘
        x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ↪[L] N
n : ℕ
R : Relations L n
x : Fin n → M
⊢ RelMap R
      ({ toFun := ↑(codRestrict (Hom.range (toHom f)) f (_ : ∀ (x : M), ↑(toHom f) x ∈ Hom.range (toHom f))),
            invFun := fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f)),
            left_inv :=
              (_ :
                ∀ (m : M),
                  (fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f)))
                      (↑(codRestrict (Hom.range (toHom f)) f (_ : ∀ (x : M), ↑(toHom f) x ∈ Hom.range (toHom f))) m) =
                    m),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Hom.range (toHom f) }),
                  ↑(codRestrict (Hom.range (toHom f)) f (_ : ∀ (x : M), ↑(toHom f) x ∈ Hom.range (toHom f)))
                      ((fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f))) x) =
                    x) }.toFun ∘
        x) ↔
    RelMap R x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
⊢ Hom.range (toHom f) = ⊤
[PROOFSTEP]
ext n
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ n ∈ Hom.range (toHom f) ↔ n ∈ ⊤
[PROOFSTEP]
simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true_iff]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ ∃ y, ↑f y = n
[PROOFSTEP]
exact ⟨f.symm n, apply_symm_apply _ _⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
⊢ Hom.range (Embedding.toHom (subtype S)) = S
[PROOFSTEP]
ext x
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ x ∈ Hom.range (Embedding.toHom (subtype S)) ↔ x ∈ S
[PROOFSTEP]
simp only [Hom.mem_range, Embedding.coe_toHom, coeSubtype]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S
[PROOFSTEP]
refine' ⟨_, fun h => ⟨⟨x, h⟩, rfl⟩⟩
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S
[PROOFSTEP]
rintro ⟨⟨y, hy⟩, rfl⟩
[GOAL]
case h.intro.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
y : M
hy : y ∈ S
⊢ ↑{ val := y, property := hy } ∈ S
[PROOFSTEP]
exact hy
