[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
⊢ F = G
[PROOFSTEP]
cases' F with Ff Fr
[GOAL]
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G
[PROOFSTEP]
cases' G with Gf Gr
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }
[PROOFSTEP]
simp only [mk.injEq]
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr
[PROOFSTEP]
exact And.intro h_fun h_rel
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F : L →ᴸ L'
⊢ LHom.id L' ∘ᴸ F = F
[PROOFSTEP]
cases F
[GOAL]
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
onFunction✝ : ⦃n : ℕ⦄ → Functions L n → Functions L' n
onRelation✝ : ⦃n : ℕ⦄ → Relations L n → Relations L' n
⊢ LHom.id L' ∘ᴸ { onFunction := onFunction✝, onRelation := onRelation✝ } =
    { onFunction := onFunction✝, onRelation := onRelation✝ }
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F : L →ᴸ L'
⊢ F ∘ᴸ LHom.id L = F
[PROOFSTEP]
cases F
[GOAL]
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
onFunction✝ : ⦃n : ℕ⦄ → Functions L n → Functions L' n
onRelation✝ : ⦃n : ℕ⦄ → Relations L n → Relations L' n
⊢ { onFunction := onFunction✝, onRelation := onRelation✝ } ∘ᴸ LHom.id L =
    { onFunction := onFunction✝, onRelation := onRelation✝ }
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L n✝), funMap (onFunction (LHom.sumElim ϕ ψ) (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L'' n✝), funMap (onFunction (LHom.sumElim ϕ ψ) (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L n✝), RelMap (onRelation (LHom.sumElim ϕ ψ) (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L'' n✝), RelMap (onRelation (LHom.sumElim ϕ ψ) (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L n✝), funMap (onFunction (sumMap ϕ ψ) (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L₁ n✝), funMap (onFunction (sumMap ϕ ψ) (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L n✝), RelMap (onRelation (sumMap ϕ ψ) (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L₁ n✝), RelMap (onRelation (sumMap ϕ ψ) (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
⊢ IsExpansionOn ϕ M
[PROOFSTEP]
letI := ϕ.defaultExpansion M
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
⊢ IsExpansionOn ϕ M
[PROOFSTEP]
refine' ⟨fun {n} f xs => _, fun {n} r xs => _⟩
[GOAL]
case refine'_1
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
f : Functions L n
xs : Fin n → M
⊢ funMap (LHom.onFunction ϕ f) xs = funMap f xs
[PROOFSTEP]
have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
[GOAL]
case refine'_1
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
f : Functions L n
xs : Fin n → M
hf : LHom.onFunction ϕ f ∈ Set.range fun f => LHom.onFunction ϕ f
⊢ funMap (LHom.onFunction ϕ f) xs = funMap f xs
[PROOFSTEP]
refine' (dif_pos hf).trans _
[GOAL]
case refine'_1
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
f : Functions L n
xs : Fin n → M
hf : LHom.onFunction ϕ f ∈ Set.range fun f => LHom.onFunction ϕ f
⊢ funMap (Exists.choose hf) xs = funMap f xs
[PROOFSTEP]
rw [h.onFunction hf.choose_spec]
[GOAL]
case refine'_2
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
r : Relations L n
xs : Fin n → M
⊢ RelMap (LHom.onRelation ϕ r) xs = RelMap r xs
[PROOFSTEP]
have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
[GOAL]
case refine'_2
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
r : Relations L n
xs : Fin n → M
hr : LHom.onRelation ϕ r ∈ Set.range fun r => LHom.onRelation ϕ r
⊢ RelMap (LHom.onRelation ϕ r) xs = RelMap r xs
[PROOFSTEP]
refine' (dif_pos hr).trans _
[GOAL]
case refine'_2
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
r : Relations L n
xs : Fin n → M
hr : LHom.onRelation ϕ r ∈ Set.range fun r => LHom.onRelation ϕ r
⊢ RelMap (Exists.choose hr) xs = RelMap r xs
[PROOFSTEP]
rw [h.onRelation hr.choose_spec]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ LHom.comp (LHom.comp e.invLHom e'.invLHom) (LHom.comp e'.toLHom e.toLHom) = LHom.id L
[PROOFSTEP]
rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ LHom.comp (LHom.comp e'.toLHom e.toLHom) (LHom.comp e.invLHom e'.invLHom) = LHom.id L''
[PROOFSTEP]
rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
⊢ card (constantsOn α) = #α
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
⊢ LHom.IsExpansionOn (LHom.constantsOnMap f) M
[PROOFSTEP]
letI := constantsOn.structure fα
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this : Structure (constantsOn α) M := constantsOn.structure fα
⊢ LHom.IsExpansionOn (LHom.constantsOnMap f) M
[PROOFSTEP]
letI := constantsOn.structure fβ
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this✝ : Structure (constantsOn α) M := constantsOn.structure fα
this : Structure (constantsOn β) M := constantsOn.structure fβ
⊢ LHom.IsExpansionOn (LHom.constantsOnMap f) M
[PROOFSTEP]
exact ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F : _)) fun n F => isEmptyElim F, fun R => isEmptyElim R⟩
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
⊢ card (L[[α]]) = lift (card L) + lift #α
[PROOFSTEP]
rw [withConstants, card_sum, card_constantsOn]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
ie : IsEmpty α
⊢ LHom.comp (LHom.sumElim (LHom.id L) (LHom.ofIsEmpty (constantsOn α) L)) (lhomWithConstants L α) = LHom.id L
[PROOFSTEP]
rw [lhomWithConstants, LHom.sumElim_comp_inl]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
ie : IsEmpty α
⊢ LHom.comp (lhomWithConstants L α) (LHom.sumElim (LHom.id L) (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id (L[[α]])
[PROOFSTEP]
simp only [LHom.comp_sumElim, lhomWithConstants, LHom.comp_id]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
ie : IsEmpty α
⊢ LHom.sumElim LHom.sumInl (LHom.comp LHom.sumInl (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id (L[[α]])
[PROOFSTEP]
exact _root_.trans (congr rfl (Subsingleton.elim _ _)) LHom.sumElim_inl_inr
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
β : Type u_1
f : α → β
⊢ comp (lhomWithConstantsMap L f) LHom.sumInl = lhomWithConstants L β
[PROOFSTEP]
ext
[GOAL]
case h_fun.h.h
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : Functions L x✝¹
⊢ onFunction (comp (lhomWithConstantsMap L f) LHom.sumInl) x✝ = onFunction (lhomWithConstants L β) x✝
[PROOFSTEP]
rfl
[GOAL]
case h_rel.h.h
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : Relations L x✝¹
⊢ onRelation (comp (lhomWithConstantsMap L f) LHom.sumInl) x✝ = onRelation (lhomWithConstants L β) x✝
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) x = ↑(Language.con L a)
[PROOFSTEP]
rw [Unique.eq_default x]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(Language.con L a)
[PROOFSTEP]
exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _
