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
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
letI := constantsOn.structure fα
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
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
letI := constantsOn.structure fβ
no goals
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
exact
  ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F : _)) fun n F => isEmptyElim F, fun R =>
    isEmptyElim R⟩