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
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
letI := ϕ.defaultExpansion M
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

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
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
refine' ⟨fun {n} f xs => _, fun {n} r xs => _⟩
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
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
have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
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
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
refine' (dif_pos hf).trans _
no goals
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
rw [h.onFunction hf.choose_spec]
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
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
have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
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
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
refine' (dif_pos hr).trans _
no goals
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
rw [h.onRelation hr.choose_spec]